stormj-UH/spivak-lean
Michael Spivak's Calculus formalized in Lean 4: every theorem and every problem of all 30 chapters and 9 appendices, in both the 3rd and 4th editions - stormj-UH/spivak-lean
2 stars · 0 forks
README
SpivakCalculus Lean 4 formalization of Michael Spivak, Calculus — both the 3rd edition (Publish or Perish, 1994) and the 4th (2008). For each edition: the whole text of Chapters 1–30 and the nine appendices (every definition, theorem, corollary and worked example, including the unnumbered examples of the running text) and every problem, in every lettered part. Problem numbers follow the 3rd edition unless marked otherwise; docs/fourth/ holds a per-chapter concordance between the two numberings.
Spivak's own definitions are used throughout: ε–δ limits and continuity, the derivative as a limit of his difference quotients, the lower/upper-sum integral, and constructions of π, sin, cos (Chapter 15), log, exp (Chapter 18), the complex numbers (Chapter 25) and the real numbers as Dedekind cuts (Chapter 29). Identification lemmas (Chapter15.piS_eq, sinS_eq, cosS_eq, Chapter18.logS_eq, expS_eq, eS_eq, rpowS_eq) prove these are Mathlib's functions, which later chapters then use. Chapter 6's ContinuousOnIccS is Spivak's own "continuous on [a, b]" (one-sided at the endpoints), and the ChapterNNContS files restate under it every theorem of the book whose hypothesis is that phrase. e is transcendental, proved twice: by Spivak's argument (Chapter21, using no Mathlib transcendence result) and by Hermite's on top of Mathlib's analytical half of Lindemann–Weierstrass (TranscendenceE). π is irrational (Chapter 16) and π is transcendental (TranscendencePi, TranscendencePiAux) — the latter by Niven's form of Hermite–Lindemann, whose algebraic half (symmetric functions of the conjugates of an algebraic number) is not in Mathlib and is proved here. Liouville's theorem on integration in finite terms (Liouville.lean, Rosenlicht's proof for differential fields) and, from it, Spivak's remark that e^{-x²} has no elementary primitive (Chapter19Liouville.lean). Mathlib had only the algebraic step of Liouville's theorem. The whole book was audited against page images of the printed 3rd edition, problem part by problem part and theorem by theorem, after the development had been written from an OCR text extraction. The results are in the ChapterNNAudit, ChapterNNText, ChapterNNAnswers and AppendixAudit files. About sixty statements are false or unusable as printed. Each is marked Correction to Spivak in its docstring and listed in PROGRESS.md; they include sixteen errors in the 3rd edition's answer section, where the development's value was right in every case; the 4th edition fixes six of them outright and keeps eight. In some twenty-six places the 4th edition independently makes exactly a correction this project had already made to the 3rd.
See PROGRESS.md for the per-chapter status of both editions, the full list of corrections, and the remaining caveats. Documentation The docstrings in the Lean sources are the documentation of record. Each theorem's docstring says what it formalizes — which numbered theorem, or which problem and lettered part, in which edition — so the sources can be read chapter by chapter alongside the book. The corrections to Spivak are recorded the same way: each is a docstring marked Correction to Spivak: on the declaration that proves the corrected statement (or that refutes the printed one). Grepping for the marker finds them all: grep -rn 'Correction to Spivak' SpivakCalculus There are 84 hits, 83 of them markers, spread over 46 files: 51 of the plain Correction to Spivak: form, 12 marked **Correction to Spivak (4th ed.), 11 **Correction to Spivak (answer section…), and the rest small variants. The same corrections are tabulated, with the reason for each, in PROGRESS.md. docs/fourth/README.md indexes the thirty 4th-edition concordance files. LICENSE and NOTICE at the repository root give the terms. The Lean code is licensed under the Apache License 2.0. NOTICE records that the underlying mathematics is Spivak's: this is an independent formalization, not affiliated with or endorsed by him or Publish or Perish, it reproduces neither the book's exposition nor its problems (they are identified by number), and a copy of the book is needed to follow it. Building lake build +SpivakCalculus # the 3rd edition (129 modules) lake build SpivakCalculus.Fourth # both editions (129 + 29 modules) SpivakCalculus.lean imports the 129 modules of the 3rd edition; SpivakCalculus/Fourth.lean imports those plus the 29 modules of the 4th. Fetch Mathlib's prebuilt artifacts first with lake exe cache get; a full build from scratch takes a few hours, most of it Mathlib. There is no sorry, no axiom and no native_decide anywhere in the project. The full axiom audit is SpivakCalculus/AuditAll.lean (not imported by either root module): lake env lean SpivakCalculus/AuditAll.lean It imports both editions, runs Lean.collectAxioms over every declaration in the Spivak namespace and reports audited 9110 declarations: all use only propext, Classical.choice, Quot.sound
SpivakCalculus/Verify.lean additionally prints the axioms of 148 representative results from Chapters 1–14 and of the transcendence of e, as a quick human-readable check. Layout All files are in SpivakCalculus/, namespace Spivak.ChapterNN; the 4th-edition files are in SpivakCalculus/Fourth/, namespace Spivak.Fourth.ChapterNN.
Chapter 3rd-edition files 4th Content
1 Chapter01 Fourth/Chapter01 Basic Properties of Numbers: P1–P12, Theorem 1, Problems 1–25
2 Chapter02, Chapter02ProblemsB Fourth/Chapter02 Numbers of Various Sorts: induction, binomial theorem, irrationality
3 Chapter03, Chapter03ProblemsB, Chapter03Audit Fourth/Chapter03 Functions; appendix on ordered pairs
4 Chapter04, Chapter04ProblemsB, Chapter04Audit, Chapter04Answers Fourth/Chapter04 Graphs; vectors, conic sections, polar coordinates
5 Chapter05, Chapter05Problems, Chapter05ProblemsB, Chapter05Text, Chapter05Audit Fourth/Chapter05 Limits (Spivak's ε–δ); the 4th edition's rewritten text
6 Chapter06, Chapter06Problems, Chapter06ProblemsB, Chapter06Text, Chapter06Audit Fourth/Chapter06 Continuous Functions; ContinuousOnIccS
7 Chapter07, Chapter07Problems, Chapter07ProblemsB, Chapter07Text, Chapter07Audit Fourth/Chapter07 Three Hard Theorems, also under Spivak's continuity
8 Chapter08, Chapter08Problems, Chapter08ProblemsB, Chapter08Text, Chapter08Audit Fourth/Chapter08 Least Upper Bounds; appendix on uniform continuity
9 Chapter09, Chapter09Problems, Chapter09ProblemsB, Chapter09Audit — Derivatives
10 Chapter10, Chapter10Problems, Chapter10ProblemsB, Chapter10Audit, Chapter10Answers Fourth/Chapter10 Differentiation, the Chain Rule
11 Chapter11, Chapter11Problems, Chapter11ProblemsB, Chapter11Appendix, Chapter11AppendixB, Chapter11Audit, Chapter11ContS Fourth/Chapter11, Fourth/Chapter11Appendix Rolle, MVT, l'Hôpital; convexity
12 Chapter12, Chapter12Problems, Chapter12ProblemsB, Chapter12Appendix, Chapter12AppendixB, Chapter12Audit, Chapter12ContS Fourth/Chapter12, Fourth/Chapter12Appendix Inverse functions; parametric curves
13 Chapter13, Chapter13Problems, Chapter13ProblemsB, Chapter13Audit, Chapter13AuditB, Chapter13ContS Fourth/Chapter13 Spivak's integral; Riemann sums
14 Chapter14, Chapter14Problems, Chapter14ProblemsB, Chapter14Audit, Chapter14ContS Fourth/Chapter14 Fundamental Theorem; improper integrals
15 Chapter15, Chapter15Problems Fourth/Chapter15 Trigonometric functions constructed
16 Chapter16, Chapter16Problems Fourth/Chapter16 π is irrational; Viète
17 Chapter17, Chapter17Area Fourth/Chapter17 Planetary motion: Kepler's laws, with the ellipse's area derived
18 Chapter18, Chapter18Problems Fourth/Chapter18 log, exp constructed
19 Chapter19, Chapter19Text, Chapter19Problems, Chapter19ProblemsB, Chapter19Appendix, Chapter19ContS, Chapter19Liouville, Liouville Fourth/Chapter19 Integration in elementary terms; Liouville's theorem; the cosmopolitan integral
20 Chapter20, Chapter20Text, Chapter20Problems, Chapter20Audit, Chapter20ContS Fourth/Chapter20, Fourth/Chapter20B Taylor's Theorem, e irrational; the 4th edition's rewritten text
21 Chapter21, Chapter21Problems, Chapter21ContS, TranscendenceE Fourth/Chapter21 e is transcendental (two proofs)
22 Chapter22, Chapter22Problems, Chapter22ProblemsB, Chapter22Audit, Chapter22ContS Fourth/Chapter22 Sequences, Bolzano–Weierstrass, Cauchy
23 Chapter23, Chapter23Problems, Chapter23ProblemsB Fourth/Chapter23 Series, rearrangements; Kempner's series
24 Chapter24, Chapter24Problems, Chapter24ProblemsB, Chapter24ProblemsC, Chapter24Audit, Chapter24ContS Fourth/Chapter24 Uniform convergence, power series
25 Chapter25, Chapter25Problems Fourth/Chapter25 Complex numbers as ordered pairs
26 Chapter26, Chapter26Problems, Chapter26Audit Fourth/Chapter26 Complex functions, Fundamental Theorem of Algebra
27 Chapter27, Chapter27Problems, Chapter27ProblemsB, Chapter27ProblemsC, Chapter27Audit Fourth/Chapter27 Complex power series, e^{iπ} = −1, Liouville's theorem, Stirling's formula
28 Chapter28, Chapter28Problems — Fields
29 Chapter29, Chapter29Problems, Chapter29Direct, Chapter29DirectB — Reals as Dedekind cuts; Cauchy sequences and decimals, all from ℚ
30 Chapter30, Chapter30Problems — Uniqueness of the reals
— TranscendencePi, TranscendencePiAux — π is transcendental
— ChapterFigures, ChapterFiguresB — the problems given only by a figure
— AppendixAudit — the text results of the nine appendices
— Bridge — Spivak's derivative and continuity agree with Mathlib's
— Verify — axioms of 148 representative results
— AuditAll — full axiom audit of every Spivak declaration
— docs/fourth/*.md — the 4th-edition concordance, one file per chapter