This project aims to formalize the first book of Euclid's Elements in Lean 4, based on the framework in A formal system for Euclid’s elements. Some of the custom tactics might be of independent interest.
The project can be used either as a standalone or as a package for other projects in Euclidean geometry, such as Pythagoras4 (whose README also contains detailed instructions on installing and running Lean 4).