GitHub - 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

GitHub

3 min read Original article ↗
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