v1.6.0 — Split Chapter 1, book-wide style pass, Python-comparison examples

Changelog — v1.6.0

← Changelog index

---

v1.6.0 — Split Chapter 1, book-wide style/consistency pass, and Python-comparison examples

The largest structural change since the chapters were first laid out.
Chapter 1 had grown to more than twice the length of any other chapter,
carrying dependent types, the full terminology glossary, and the formal
calculus-of-constructions material all under one roof. It is now two
chapters, and the book took the opportunity to clear a long-standing
style backlog, fix several numbering regressions the split introduced,
balance a thin chapter, and add a Python-comparison worked example to
every main chapter that lacked one.

Structural changes

• Chapter 1 split into two. The old Chapter 1 (01-basics) is now
  Chapter 1, "Basics" (#eval, def, dependent types, Vec), and a new
  Chapter 2, "Terminology and the calculus of constructions"
  (02-terminology-and-coc), carrying the glossary and the formal Π/Σ-type
  material. Every later chapter, every cross-reference, the README table
  of contents, learning-paths.md's dependency graph, the appendix
  solutions folder, and tactic-and-library-reference.md were renumbered
  and re-linked accordingly.
• Chapter 3 balanced. Chapter 3 ("Functions, definitions, and
  structures") was the one chapter without an exercises section. It now
  has one (03-functions-and-structures/04-exercises.md, 3 new
  exercises: Rectangle/area, Box α/unwrap, ColoredRectangle
  extending Rectangle), with a matching appendix-solutions file
  (15-appendix-solutions/03-chapter-3.md). This shifted the appendix
  numbering for every chapter after it (04-chapter-4.md through
  12-chapter-12.md), renumbered and re-linked from the 11 chapters that
  reference their own solutions file.

Fixes

• A book-wide backlog of roughly 145 prose colons, em-dashes, and English
  possessives, cleared across ~61 files (excluding the changelog and code/
  math spans), completing the style rule the v1.5.3 pass started.
• Chapter 0's title ("Setting up Lean 4") had regressed to "Chapter 1"
  after the split; fixed.
• Appendix solutions off-by-one. Every appendix file from the old
  "Chapter 4" solutions onward had its heading, nav, and in-body "Chapter
  N" citations numbered one chapter too high relative to its own filename,
  a regression from the split's renumbering script. Fixed across all 9
  affected files, verified against real content (e.g. confirmed
  Perm3.ext is genuinely in Chapter 7).
• A broken "back" nav link in 03-functions-and-structures/00-index.md
  still pointing at the old, pre-split Chapter 1.
• learning-paths.md mis-citing "Chapter 1, Section 1" for what is now
  Chapter 0's "Why Lean?", and a merged sentence incorrectly attributing
  both toolchain-check and Fin/Vec content to the same chapter.
• The README's checkpoint-project description ("after Chapter 5 and
  after Chapter 11") and appendix link (14-appendix-solutions/), both
  stale by one chapter after the split.
• 96 stale .tex files left over from the pre-split LaTeX directory
  layout, removed.

Additions

• Ten new "Programmer's corner (Python)" boxes, one in each of
  Chapters 3, 4, 7, 8, 9, 10, 11, 12, 13, and 14 (every main chapter that
  previously lacked one), each grounding the value of Lean and functional
  programming in a concrete, specific Python bug rather than an abstract
  claim: an untyped dict KeyError and mutable-dataclass aliasing
  (Ch. 3), a runtime assert versus a proof-carrying precondition
  (Ch. 4), an unchecked "group" class built from subtraction (Ch. 7), a
  test sampling one case versus a proof holding for every case (Ch. 8),
  float silently breaking associativity (Ch. 9, plus the pre-existing
  by decide box renumbered to its correct section), nan breaking the
  absorbing law mul_zero proves unconditionally (Ch. 10), duck-typed
  __mul__/__rmul__ scalar/vector mismatches versus smul's fixed type
  (Ch. 11), a hand-checked graph-path invariant nobody remembered to
  re-verify everywhere (Ch. 12), omega deciding a universal statement
  versus assert sampling one pair (Ch. 13), and a capstone box in
  Ch. 14 tying the whole recurring theme together, invariants as types
  instead of conventions.
• The Python companion notebook (python-companion/python_companion.ipynb)
  rewritten to match, with corrected chapter/section references for every
  pre-existing cell and 10 new runnable cells for the boxes above, every
  cell verified to execute.

Process note

REPRODUCING.md gained a new step describing this pass, for anyone
replaying the book's construction from scratch.

Post-release follow-up (same book content, no PDF changes)

A few loose ends were closed on master right after this tag was cut,
none of which change the book text or the compiled PDF:

• Ported the new Chapter 3 exercise solutions (Rectangle/area,
  Box/unwrap, ColoredRectangle) and the Chapter 1 vecLen/vecLen'
  comparison into lean_project/, and verified them, along with the
  entire project (8681 jobs, including every Mathlib-dependent module),
  with a clean lake build. This closed issues #242
  and #246.
• Closed issue #243
  (cutting a standalone v1.5.4 release), superseded by this release.
• Backfilled PROJECT-HISTORY.md with the 34 merged PRs (#161–#247)
  it was missing.

Compare v1.5.3...v1.6.0

---

← Changelog index