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 

 If you want a non Coq proof of \(2 + 2 = 4\), check here
 If you want to learn more about Coq, try the book Software Foundations
 Check out Coq on your browser
 Formalization of 100 Theorems in Coq
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. – Pi Han Goh · 1 month, 1 week ago
Log in to reply