Inspiration: Another Test Problem from Kelly's Group.
Coq is an interactive proof assistant. What this means is that Coq helps you prove theorems in a way that can be mechanically checked by Coq itself. This technology could be used to prove mathematical theorems, or develop formally correct software.
A famous example of a notorious theorem whose formal proof was developed in Coq is the four color theorem (download the proof here). Also, it has been used to generate a formally correct C compiler, which is pretty cool, if you think about it.
Behold we prove $2 + 2 = 4$ in Coq as a teaser
To run the proof below, you'll need Coq. You can read more about the Coq Proof Assistant on Wikipedia
We shall begin by defining the natural numbers along with two
and four
.
1 2 3 4 5 6 

We then, define plus
1 2 3 4 5 6 7 8 

Now, we can prove the theorem we desire.
1 2 3 

And we are done!
Alternately, you could also use this:
1 2 

Problem Loading...
Note Loading...
Set Loading...
$</code> ... <code>$</code>...<code>."> Easy Math Editor
*italics*
or_italics_
**bold**
or__bold__
paragraph 1
paragraph 2
[example link](https://brilliant.org)
> This is a quote
2 \times 3
2^{34}
a_{i1}
\frac{2}{3}
\sqrt{2}
\sum_{i=1}^3
\sin \theta
\boxed{123}
Comments
Sort by:
Top NewestAnother marvelous proof, you couldn't have eludicated any clearer!
I was thinking of proving 2+2=4 using accelerated course, but yours is definitely far superior to mine.
Log in to reply