A Lean 4 formalization of classical geometry, following Greenberg’s Euclidean and Non-Euclidean Geometries.
You can find a cool rendering of all the proofs at this site. This uses Atlas which is a custom rendering frontend thing for Lean.