The geometric kernel is written in Lean and is thus also verified by the Lean prover.