# 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. Commented May 1, 2014 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
Commented May 1, 2014 at 12:11
• See this answer and this for a few examples in propositional calculus. Commented May 1, 2014 at 12:13