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

Category: other

Tags: lean4, formal-verification, mathematics, calculus, theorem-proving

Score: 7.8/10 (Innovation: 8, Technical: 9, Documentation: 8, Utility: 6)

A complete Lean 4 formalization of Michael Spivak's Calculus, covering every theorem and problem from both the 3rd and 4th editions, including corrections to statements and answers. It stands out for its rigorous audit against the printed text, independent proofs of transcendence results, and notable contributions to Mathlib such as Liouville's theorem on integration in finite terms.

Target audience: mathematicians, proof assistants researchers, computer scientists interested in formal verification, educators

Repository: https://github.com/stormj-UH/spivak-lean · Lean · Apache-2.0 · 45 stars

View on Hacker News