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

Show HN: Spivak's Calculus formalized in Lean 4 – every theorem, every problem stormj-UH / spivak-lean Public Notifications You must be signed in to change notification settings Fork 0 Star 2 Branches Tags Open more actions menu Latest commit History 29 Commits 29 Commits Folders and files Name Name Last commit message Last commit date SpivakCalculus SpivakCalculus docs/ fourth docs/ fourth .gitignore .gitignore LICENSE LICENSE NOTICE NOTICE PROGRESS.md PROGRESS.md README.md README.md SpivakCalculus.lean SpivakCalculus.lean lake-manifest.json lake-manifest.json lakefile.toml lakefile.toml lean-toolchain lean-toolchain Repository files navigation 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.

This Other is relevant to the technology intelligence record because it involves DeveloperTools activity. The source article should remain the factual reference for follow-up coverage.

• stormj-UH / spivak-lean Public Notifications You must be signed in to change notification settings Fork 0 Star 2 Branches Tags Open more actions menu Latest commit History 29 Commits 29 Commits Folders and files Name Name Last commit message Last commit date SpivakCalculus SpivakCalculus docs/ fourth docs/ fourth .gitignore .gitignore LICENSE LICENSE NOTICE NOTICE PROGRESS.md PROGRESS.md README.md README.md SpivakCalculus.lean SpivakCalculus.lean lake-manifest.json lake-manifest.json lakefile.toml lakefile.toml lean-toolchain lean-toolchain Repository files navigation 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.