siqiliu-tsinghua / tautology

Real analysis formalized in Lean 4 from nothing — the reals are constructed here. No mathlib, no external dependencies, no typeclasses.