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