aleradLeanCert0.1.0

Verified interval arithmetic for Lean 4 — prove bounds on exp, sin, cos, find roots, all machine-checked
Displaying 1-5 of 5 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. deancureton/MovingSofausesv4.33.0.1

    Autoformalization of Baek's solution to the moving sofa problem: the Gerver sofa is optimal

  5. AlexKontorovich/PrimeNumberTheoremAndusesv4.34.0

    Blueprint for the PNT+ Project