A complete Lean 4 formalization of Michael Spivak's Calculus: all 30 chapters, 9 appendices, and every problem, in both the 3rd (1994) and 4th (2008) editions. 159 files, ~115,000 lines, 9,068 declarations depending only on propext, Classical.choice and Quot.sound. No sorry, no added axioms.
It uses Spivak's definitions rather than Mathlib's, so the three hard theorems come out of his ε–δ and least-upper-bound arguments, and the integral is his Darboux construction.
Two results here aren't in Mathlib: π is transcendental (Niven's proof; Mathlib has only the analytic half of Lindemann–Weierstrass), and Liouville's theorem on integration in finite terms, giving that e^(−x²) has no elementary primitive — elementarity in the differential-field sense, with the translation from arbitrary real expressions not formalized.
The audit found errors in the book. I first worked from an OCR text extraction, then checked every problem against page images. That caught dropped primes and radicals that had me proving the wrong problem — and 83 places where Spivak's statement is wrong as printed, each recorded in a docstring and formally refuted where it's false.
Eleven are wrong answers in the 3rd edition's answer key. For Σ n!zⁿ/nⁿ he computes a limit as 0 and concludes the radius of convergence is infinite; since ⁿ√(n!)/n → 1/e, it's e. Elsewhere: 12 terms claimed to give e² to within 10⁻⁵ (they don't), a sign error contradicting his own derivation on the next page, a Taylor coefficient reported as a derivative.
The check on my own work: in 26 places Spivak's 4th edition independently makes exactly the correction I'd already made to the 3rd. We converged, separately, on the same list.
The audit also caught one of my own mistakes: Spivak defines "continuous on [a,b]" with one-sided limits at the endpoints, and I'd used two-sided, which silently constrains the function outside the interval. Rolle, the MVT, both parts of the FTC and the rest are now proved under his actual hypothesis; three came out strictly stronger.
The English write-up isn't in the repo — it renders nearly every problem as prose, which is Spivak's to publish. The docstrings are the documentation. Code is Apache 2.0; you need the book to follow it.
A complete Lean 4 formalization of Michael Spivak's Calculus: all 30 chapters, 9 appendices, and every problem, in both the 3rd (1994) and 4th (2008) editions. 159 files, ~115,000 lines, 9,068 declarations depending only on propext, Classical.choice and Quot.sound. No sorry, no added axioms.
It uses Spivak's definitions rather than Mathlib's, so the three hard theorems come out of his ε–δ and least-upper-bound arguments, and the integral is his Darboux construction.
Two results here aren't in Mathlib: π is transcendental (Niven's proof; Mathlib has only the analytic half of Lindemann–Weierstrass), and Liouville's theorem on integration in finite terms, giving that e^(−x²) has no elementary primitive — elementarity in the differential-field sense, with the translation from arbitrary real expressions not formalized.
The audit found errors in the book. I first worked from an OCR text extraction, then checked every problem against page images. That caught dropped primes and radicals that had me proving the wrong problem — and 83 places where Spivak's statement is wrong as printed, each recorded in a docstring and formally refuted where it's false.
Eleven are wrong answers in the 3rd edition's answer key. For Σ n!zⁿ/nⁿ he computes a limit as 0 and concludes the radius of convergence is infinite; since ⁿ√(n!)/n → 1/e, it's e. Elsewhere: 12 terms claimed to give e² to within 10⁻⁵ (they don't), a sign error contradicting his own derivation on the next page, a Taylor coefficient reported as a derivative.
The check on my own work: in 26 places Spivak's 4th edition independently makes exactly the correction I'd already made to the 3rd. We converged, separately, on the same list.
The audit also caught one of my own mistakes: Spivak defines "continuous on [a,b]" with one-sided limits at the endpoints, and I'd used two-sided, which silently constrains the function outside the interval. Rolle, the MVT, both parts of the FTC and the rest are now proved under his actual hypothesis; three came out strictly stronger.
The English write-up isn't in the repo — it renders nearly every problem as prose, which is Spivak's to publish. The docstrings are the documentation. Code is Apache 2.0; you need the book to follow it.
reply