Built on Lean 4 + Mathlib
LucidMath
LucidMath is the Institute's formal-verification engine: a library of mathematics written in Lean 4 and Mathlib in which every theorem is checked, line by line, by a proof kernel. When LucidMath certifies a result, a machine has re-derived it from the axioms and would reject a single wrong step. A green build is the proof.
What Makes It Trustworthy
Kernel-Checked, Not Asserted
Every claim reduces to a proof the Lean kernel accepts, on the standard mathematical axioms and nothing more. Hidden gaps and stray axioms are detected automatically and fail the build.
Honest Status Taxonomy
A result is either proved (kernel-checked), an axiom-audit (a structural-consistency scaffold, explicitly not a proof of philosophy), or resolved (a real error caught and corrected, with the counterexample kept as a permanent guard). These are never blurred.
One Claim, Three Places, Enforced
Each result carries a stable identifier linking its Lean proof, its registry entry, and the badge in the published manuscript. CI fails if any of the three drift apart.
It Finds Real Mistakes
LucidMath has already caught and corrected published errors (a credit-cycle formula and an economic inequality among them), turning each into a guarded, kernel-checked fact.