hanwenzhuLeanArchitect

LeanArchitect extracts a blueprint directly from Lean source.
Displaying 1-7 of 7 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. subfish-zhou/goldbachusesv4.33.0-rc1

    A Lean 4 formalization of Chen's theorem (Goldbach 1+2).

  4. emilyriehl/InfinityCosmosusesv4.33.0-rc1

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

  5. formal-applied-math/MathFinusesv4.33.0-rc1

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

  6. AxiomMath/PrimeGapsLibusesv4.32.0-rc1

    Lean formalization of bounded gaps between primes

  7. AlexKontorovich/PrimeNumberTheoremAndusesv4.32.0-rc1

    Blueprint for the PNT+ Project