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
    Commented May 1, 2014 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
    Commented May 1, 2014 at 12:11
  • 1
    $\begingroup$ See this answer and this for a few examples in propositional calculus. $\endgroup$
    – Git Gud
    Commented May 1, 2014 at 12:13

1 Answer 1


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/


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .