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 

Easy Math Editor
This discussion board is a place to discuss our Daily Challenges and the math and science related to those challenges. Explanations are more than just a solution — they should explain the steps and thinking strategies that you used to obtain the solution. Comments should further the discussion of math and science.
When posting on Brilliant:
*italics*
or_italics_
**bold**
or__bold__
paragraph 1
paragraph 2
[example link](https://brilliant.org)
> This is a quote
\(
...\)
or\[
...\]
to ensure proper formatting.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