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.