EG. Formalizing Euclidean Geometry in Lean
mathlib4. Lean
neukirch. Lean
CPAlgClosed. C_p is algebraically closed in Lean 4
