Show HN: Spivak's Calculus formalized in Lean 4 – every theorem, every problem

A GitHub project formalizes Michael Spivak's Calculus in Lean 4, covering both the 3rd and 4th editions: the complete text of Chapters 1-30, nine appendices, every definition, theorem, corollary, worked example and every problem. It follows Spivak’s own ε-δ limits, the derivative as a limit of difference quotients, and the lower/upper-sum integral, and constructs π, sin, cos, log, exp, the complex numbers and the real numbers as Dedekind cuts. Major results include two independent proofs that e is transcendental (one following Spivak, one via Hermite on top of Mathlib’s Lindemann-Weierstrass), proofs that π is irrational and transcendental, Liouville’s theorem on integration in finite terms and the nonexistence of an elementary primitive for e^(−x^2). Identification lemmas tie these constructions to Mathlib’s functions, and the development avoids sorry, extra axioms and native_decide.

The entire formalization was audited against page images of the printed 3rd edition; roughly sixty printed statements were found false or unusable and are documented as corrections in docstrings and in PROGRESS.md. Every Lean declaration’s docstring records which numbered theorem or problem it formalizes so the sources can be read alongside the book. The project includes build instructions (lake), an axiom audit reporting 9,110 declarations using only propext, Classical.choice and Quot.sound, and is released under Apache‑2.0 with a NOTICE that the mathematics is Spivak’s and a copy of the book is required to follow the material.