The following is a collection of variou results in planar Euclidean Geometry formalised via Lean 4. Euclidean Geometry is defined via complex numbers and everything proven from scratch; in particular without mathlib. Notably, this project contains a proof of Ceva's theorem (+ converse), which is situated in the Ceva.lean file. The final statement is at the very bottom of the file (theorem ceva).
Further overview of the project is described in README.lean