ProjectIdeas
Now that you know the basics of Coq you are itching to prove something. Here are some ideas.
Other than formalizing existing proofs, one useful exercise is to update some of Coq's user-contributed libraries so that they build on the recent additions in the Coq StandardLibrary rather than their own foundations.
See Top100MathematicalTheoremsInCoq and Formalizing 100 Theorems
forall (x y z:Z), x^3 + y^3 = z^3 -> x=0 \/ y= 0 \/ z=0
See Fermat's Last Theorem: Proof for n=3.
http://nshmyrev.narod.ru/temp/fermat4.tar.gz start of the proof.
|{}| |{}| |{o}| |{o}| |{o}| |{o}| |{o}| |{o}| (change the estimate if you disagree)
(none)
forall (x y z:Z) (n:nat), x^(n+3) + y^(n+3) = z^(n+3) -> x=0 \/ y= 0 \/ z=0
Fermat's last theorem has been proven in Coq for the n=4 case. The proof is available in UserContributions/CNAM/Fermat4/ .
See also, Computer verification of Wiles' proof of Fermat's Last Theorem
|{}| |{}| |{}| |{}| |{}| |{}| |{}| |{}| (change the estimate if you disagree)
(none)
Any strongly disjoint pair of analytic sets is strongly Borel sepearable.
Peter Aczel has a proof in constructive ZF. It should be possible to translate this proof into type theory.
|{}| |{}| |{}| |{}| |{o}| |{o}| |{o}| |{o}| (change the estimate if you disagree)
The maximal length of an atom in the splitting of a 50-day-old string is 74. Every such atom decays, in at most 17 days, into stable or transuranic elements.
http://www.cs.cmu.edu/~kw/pubs/conway.pdf http://www.mathematik.uni-bielefeld.de/~sillke/SEQUENCES/series000
??? (change the estimate if you disagree)
(none)
This has now been completed by Wouter Stekelenburg.
This has now been completed. See http://coqprime.gforge.inria.fr/
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.