hanwenzhuLeanArchitect

LeanArchitect extracts a blueprint directly from Lean source.
Displaying 1-8 of 8 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

    The Lean Financial Mathematics Library

  6. AxiomMath/PrimeGapsLibusesv4.32.0-rc1

    Lean formalization of bounded gaps between primes

  7. AlexKontorovich/PrimeNumberTheoremAndusesv4.34.0

    Blueprint for the PNT+ Project

  8. AxiomMath/PrimeNumberTheoremAndusesv4.32.0-rc1

    Axiom fork of https://github.com/AlexKontorovich/PrimeNumberTheoremAnd