Real analysis formalized in Lean 4 from nothing — the reals are constructed here. No mathlib, no external dependencies, no typeclasses.
-
Updated
Aug 19, 2026 - Lean
#
mathlib-free
Here are 2 public repositories matching this topic...
A machine-checked post-quantum memory bound in Lean 4 — 20 theorems, 0 sorry, 0 imports, mathlib-free
-
Updated
Aug 18, 2026 - Lean
Add this topic to your repo
To associate your repository with the mathlib-free topic, visit your repo's landing page and select "manage topics."