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