hanwenzhuLeanArchitect

LeanArchitect extracts a blueprint directly from Lean source.
Displaying 1-5 of 5 packages depending on hanwenzhu/LeanArchitect
Sort by

  1. kim-em/ErdosUnitDistanceusesv4.32.0-rc1

    Formalization of Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture (companion to mathlib4 branch kim/erdos-unit-distance)

  2. kim-em/ErdosUnitDistanceComparatorusesv4.32.0-rc1

    Independent comparator verification: the uniform-constant Erdős unit-distance conjecture is false (Alpöge 2026, formalized)

  3. emilyriehl/InfinityCosmosusesv4.33.0-rc1

    A blueprint for a formalization of infinity-cosmos theory in Lean.

  4. formal-applied-math/MathFinusesv4.32.0

    Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

  5. AlexKontorovich/PrimeNumberTheoremAndusesv4.32.0-rc1

    Blueprint for the PNT+ Project