aleradLeanCert0.1.0

Verified interval arithmetic for Lean 4 — prove bounds on exp, sin, cos, find roots, all machine-checked
Displaying 1-4 of 4 packages depending on alerad/LeanCert
Sort by

  1. kim-em/ErdosUnitDistanceusesv4.32.2.4

    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.2.4

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

  3. bjoernkjoshanssen/interestusesv4.31.0

    Interest: a Lean library for financial mathematics

  4. AlexKontorovich/PrimeNumberTheoremAndusesv4.32.2.4

    Blueprint for the PNT+ Project