I'm looking for a nice example of a formal proof of some well-known mathematical fact.

I know about Mizar project, but I'd rather prefer something like this nice proof of $1+1=2$ which uses first-order logic.

I'm also familiar with Metamath, it is cool (scary, but cool).

Is there any other examples of nice formal proofs (some geometry examples would be awesome)?

  • 1
    $\begingroup$ I don't understand if you want a list of formal proofs, if you want a formal proof of $1+1=2$ or something else. Plus, formal proofs require formal systems, i.e., a general setting in which what is a 'statement' is something which is defined and the same goes for 'proof'. You also need axioms and deduction rules. You've provided none of these. All of this makes the question very unclear. $\endgroup$ – Git Gud May 1 '14 at 12:06
  • $\begingroup$ I want examples of formal proofs. Let it be "lists". And I've provided an example which uses first-order predicate calculus. I'm quite sure, it is a formal system. $\endgroup$ – sas May 1 '14 at 12:11
  • 1
    $\begingroup$ See this answer and this for a few examples in propositional calculus. $\endgroup$ – Git Gud May 1 '14 at 12:13

Freek Wiedijk has a list of 100 famous theorems and link to their formalization in different proof assistants (http://www.cs.ru.nl/~freek/100/). The list includes some geometric theorems: Desargues theorem, Pythagorean theorem, area of circle, Feuerbach...

If you want some synthetic proofs of some well known geometric theorems starting from the axioms you can have a look at our formalization based on Tarski's axiom system: http://geocoq.github.io/GeoCoq/


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.