hanwenzhuLeanArchitect

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

  1. mo271/Aperyusesv4.33.0

  2. amellendijk/BVusesv4.35.0

    A Lean blueprint documenting a formalization of Bombieri-Vinogradov

  3. 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)

  4. kim-em/ErdosUnitDistanceComparatorusesv4.32.0-rc1

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

  5. subfish-zhou/goldbachusesv4.33.0-rc1

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

  6. emilyriehl/InfinityCosmosusesv4.33.0-rc1

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

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

    The Lean Financial Mathematics Library

  8. AxiomMath/PrimeGapsLibusesv4.32.0-rc1

    Lean formalization of bounded gaps between primes

  9. AlexKontorovich/PrimeNumberTheoremAndusesv4.35.0

    Blueprint for the PNT+ Project

  10. AxiomMath/PrimeNumberTheoremAndusesv4.32.0-rc1

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

  11. Stavan-Jain/QECusesv4.30.0-rc2

    Formalization project on Quantum Error Correction in Lean