# Formal proof of famous theorem

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)?

• 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. – Git Gud May 1 '14 at 12:06
• 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. – sas May 1 '14 at 12:11
• See this answer and this for a few examples in propositional calculus. – Git Gud May 1 '14 at 12:13

## 1 Answer

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/