aleradLeanCert0.1.0

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

  1. mo271/Aperyusesv4.33.1

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

  3. kim-em/ErdosUnitDistanceComparatorusesv4.32.2.4

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

  4. bjoernkjoshanssen/interestusesv4.31.0

    Interest: a Lean library for financial mathematics

  5. deancureton/MovingSofausesv4.33.0.1

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

  6. AlexKontorovich/PrimeNumberTheoremAndusesv4.35.0

    Blueprint for the PNT+ Project