v1.6.1 — Companion-project verification and history backfill

Changelog — v1.6.1

← Changelog index

---

v1.6.1 — Companion-project verification and history backfill

A follow-up to v1.6.0, closing loose ends discovered while auditing it.
No book text or worked example changed; this release covers the
companion Lean project and repository meta-documentation only.

Fixes

• lean_project gaps closed. Two code blocks the book claims are
  "ported into lean_project/ and verified with lake build" had never
  actually been ported: the Chapter 3 exercise solutions
  (Rectangle/area, Box/unwrap, ColoredRectangle) added in
  v1.6.0, and the Chapter 1, Section 3 vecLen/vecLen' comparison.
  Both are now in lean_project/LeanProject/, and every #eval/#check
  output was checked to match the book exactly.
• Full project build verified. A complete lake build (8681 jobs,
  including every Mathlib-dependent module) passes clean against
  master post-Chapter-1-split, resolving issue
  #246.
  This also resolves issue
  #242.
• Closed issue #243
  (cutting a standalone v1.5.4 release), superseded by v1.6.0.
• Root README off-by-one. "Mathlib equivalent" boxes actually start
  in Chapter 7 (07-groups/), not Chapter 6 as the README said in two
  places, the same pre-split-regression pattern already fixed for the
  checkpoint-project reference in v1.6.0.

Housekeeping

• PROJECT-HISTORY.md backfilled. Its merged-PR table had stopped
  at #159; added the 34 PRs merged since (through v1.6.0/#247), updated
  the issue/PR counts (97 issues → 148, 63 PRs → 97), and added a
  summary bullet for the v1.6.0 work.

Compare v1.6.0...v1.6.1

---

← Changelog index

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

v1.5.3 — Book-wide prose style pass: no colons, em-dashes, or possessives

Full editorial pass over every chapter (1–14), the appendix solutions, and the front-matter reference pages, rewriting prose to avoid colons and em-dashes (ambiguous against Lean's own : type ascription and -- line-comment syntax) and English possessive ('s) constructions. Code blocks, LaTeX math, chapter/section titles, and direct quotes from external sources are untouched. The changelog directory was left out of scope, since it is release history rather than reader-facing narrative prose.

See lean_book/changelog/v1.5.3.md for the full changelog entry.

v1.5.2 — Corrections from the 2026-08-03/run-173410 closing review

Changelog — v1.5.2

← Changelog index

---

v1.5.2 — Corrections from the 2026-08-03/run-173410 closing review

A second closing-review pass (reviews/2026-08-03/run-173410/) ran the same
multi-model panel-then-adjudication pipeline again — six Phase-1 reviewers,
four Phase-2 cross-critiques, five specialized reviewers (category theory,
notation, proof search, Lean audit, typesetting) — adjudicated into one
fix-ready report. This release applies the confirmed findings from that
report, all re-verified against the working tree before being applied.

Mathematical and category-theoretic corrections

Chapter 11, Section 5 — the free-category associativity claim was false.
The prose said the cons case of Path.append's recursion "is exactly
associativity of concatenation." It is not: that case is a definitional
recursion lemma used to unfold Path.append one arrow at a time, not a
proof that composition is associative. True associativity is now stated
explicitly, with the correct induction argument — on the third path
argument, matching Path.append's own recursion on its second argument
(the adjudicated report's own suggested fix direction, induction on the
first argument, was itself checked against the Lean source and found
incorrect; corrected here).

Chapter 11 — the free-category universal property is now stated in
full. The book named "universal property" without formulating it. It now
states $\mathrm{Hom}{\mathbf{Cat}}(\mathrm{Free}(Q), C) \cong
\mathrm{Hom}{\mathbf{Quiv}}(Q, U(C))$ explicitly, with $U$ named as the
forgetful functor $\mathbf{Cat} \to \mathbf{Quiv}$.

Chapter 11 index and Section 5 — composition verification claims were
overstated. A single rfl check on one concrete instance
(pathBetaAlphaViaAppend = pathBetaAlpha) was described as if it verified
associativity and identity laws in general. Both now qualify the claim to
the single concrete check it actually is.

Chapter 1, Section 4 — ℕ mislabeled as the initial object of Type.
The terminology box conflated Nat.rec's uniqueness (which comes from ℕ
being the initial $F$-algebra / natural number object for the successor
endofunctor) with the initial object of Type itself (the empty type).
Corrected, with a cross-reference to Section 1's existing $F$-algebra/NNO
discussion, which already had this right.

Chapter 1, Section 4 — forgetful functor table cited nonexistent Lean
fields. The table claimed Ring → Group uses r.toGroup and
Group → Set uses g.carrier; neither field exists. Verified against
Ch08Rings.lean: the real chain is r.addGrp (Ring → CommGroup) then
.toGroup (CommGroup → Group, from extends); Group's carrier is the
type parameter G itself, not a projected field.

Faithfulness and exercise-solution fixes

• Chapter 7, Theorem 1 (id_unique) — the book presented this proof
  with sorry; replaced with the actual compiling proof.
• Chapter 10, linear maps — the claim that composition/identity
  linearity are "easy to prove" pointed at nothing; the appendix already
  proves both (idLinearMap, composeLinearMap), now cross-referenced
  instead of left dangling.
• Appendix, Chapter 3 — ⟨1, rfl⟩ was offered as an alternative proof
  of 1 > 0; it does not compile on Lean 4.32.2 (1 > 0 is propositional,
  not definitional, equality). Corrected to ⟨1, Nat.one_pos⟩ with an
  explanation tying back to Chapter 5.
• Appendix, Chapter 11 — the Path.cons Infoview description in the
  solutions appendix didn't match the actual tactic state (fixed variable
  vs. auto-generated intermediate vertex). Corrected.
• Appendix, Chapter 10, Exercise 3 — now flagged explicitly as a
  partial solution (natural-scalar case only; the Int case is left as an
  exercise).
• Appendix, Chapter 11, Exercise 1 — now notes explicitly that the
  solution builds a fresh CyclicArrow/cyclicQuiver rather than
  extending the book's own ExampleArrow.
• Chapter 3, exercises — a Socratic answer claimed rfl cannot prove
  ∀ n, n + 0 = n; it can (Nat.add recurses on its second argument, so
  this is the base case). The genuinely unprovable statement is
  0 + n = n. Corrected.
• Minor proof-search narrative sharpening in Chapter 7 (Theorems 1–3) and
  Chapter 9 (Theorem 1–2): a lemma-availability claim, an Eq.symm
  metaphor, and an rw-failure anecdote misattributed to the wrong proof
  step.

Reference tables

• · disambiguated into two rows (Group.op, Chapter 6, vs. SMul,
  Chapter 10) with an explanatory note — same math notation, two different
  Lean operations depending on context.
• ⟶ was listed as "Chapter 1, never used"; it is used, in Chapter 11 —
  first-appearance column corrected instead of removed.
• Added missing entries: ¬ (lambda-calculus dictionary), ↑ coercion,
  ⊕ direct sum, a dedicated rfl row distinguishing tactic-use
  (Chapter 1) from proof-term-use (Chapter 3).
• Corrected ⟨_, _⟩ first-appearance from Chapter 2 to Chapter 1.
• Lambda-calculus dictionary's Σ-type row, which conflated structure
  with ∃, split into separate rows.

Front matter and documentation

• README.md, lean_book/README.md: removed a promised "ring as a
  one-object preadditive category" viewpoint that doesn't exist anywhere
  in Chapter 8 or the book; removed a stale claim that learning objectives
  are "never listed explicitly" (v1.5.0 added Learning objectives boxes to
  every chapter).
• REPRODUCING.md: fixed an invalid unquoted TOML value in prose
  (rev = v4.32.2 → rev = "v4.32.2"; the real lakefile.toml was
  already correctly quoted).
• Fixed a stale chapter/section cross-reference in Chapter 13's next-steps
  material (pointed at Chapter 11 Section 1 instead of Section 3) and a
  pronoun-ambiguity fix in the same file's Church-numeral discussion.
• Fixed a wrong Chapter 6/Chapter 7 theorem cross-reference in the Chapter
  6 exercises.
• NOTICE.md, lean_book_latex/frontmatter.tex: removed the "free-tier"
  qualifier from the AI-model review-panel description (the models
  themselves are unaffected; this was a wording-only fix), and removed
  the paragraph describing the reviews/2026-08-02/ round now that that
  directory has been removed from the repository.

Notes

• Every fix landed in the Markdown source; lean_book_latex/ was
  regenerated from it via build_latex.py. No .tex chapter file was
  hand-edited. preamble.tex and frontmatter.tex, which are hand-
  maintained (not generated), were edited directly.
• The .tex-only typesetting defects from the same review round
  (Infoview image overflow, bibliography URL overflow, glue-shrinkage
  errors, overfull hboxes, bibliography chapter-numbering collision) are
  not fixed in this release — they require direct edits to
  preamble.tex/bibliography.tex beyond a markdown regeneration and
  remain open.
• reviews/2026-08-02/ was removed from the repository in this release.
• The fixes themselves have not had a further adversarial re-review.
  Discrepancies found in the adjudicated report itself while applying its
  findings are documented in that report's POST-HOC CORRECTIONS section
  (reviews/2026-08-03/run-173410/p3-adjudication/FINAL-REVIEW.md).

v1.4.24 — Full-book AMS-style rigor and narrative pass

Rigor audit (4 parallel review passes, every Lean snippet cross-checked against the pinned toolchain): fixed wrong error-message quotes, a wrong #print Fin field type, a missing paren in a #eval output, an internal Group (α) vs Group (G) inconsistency, a date inconsistency for Gödel's completeness result, a wrong exercise cross-reference, and a fabricated universe-formation exception. Chapters 6–14 (23 files) audited with no defects found.

Narrative rewrite: every section's formal-citation box moved from the top (the reader's first impression) to a "Sources, quoted" recap at the bottom, with genuine connective prose replacing it. Every chapter index gained a "story of this chapter" arc. The former separate "References" list was merged into "Sources, quoted". The informal "Brief:" gloss following each verbatim quote was renamed "Picture it like this:" and rewritten as a plain-language, real-world analogy (customs stamps, airport security, kitchen recipes, staircases, Lego manuals, litmus tests, and more), while every quote/citation stays fully rigorous.

Repo layout: moved the generated LaTeX tree from lean_book/latex/ to a top-level sibling, lean_book_latex/. Cleanup: removed references to internal, gitignored verification files from reader-facing book text.

Full details in CHANGELOG v1.4.24.

Includes a source-bundle asset (-source.zip) alongside the PDF, per the usual release format.

v1.4.23 — Add dbg_trace tracing to every genuinely recursive Lean block

Completes the dbg_trace initiative: every Lean code block in the book was surveyed chapter by chapter, and every genuine recursion now has a dbg_trace-annotated sibling definition showing the computation unwind one step at a time.

• Chapter 1 (pattern-setting installment): Vec.replicate, Vec.dot, double (via Nat.rec). Also documents a real limitation found along the way — myLength (via List.rec/#reduce) cannot be traced at all, since kernel reduction skips dbg_trace's side effect entirely.
• Chapter 10: natSmul.
• Chapter 11: Path.append and Path.length, traced together since Path has no Repr instance to observe Path.append in isolation.
• Chapter 14: the corresponding exercise-solution mirrors of the above.
• Chapters 2–9, 12, 13 confirmed to need no changes — surveyed and found to contain only non-recursive structures, instances, and tactic-mode proofs.

Full details in CHANGELOG v1.4.23.

Includes a source-bundle asset (-source.zip) alongside the PDF, per the usual release format.

v1.4.22 — Book-wide content-quality pass

Book-wide content-quality pass gathered from reader feedback, shipped as several PRs:

• Quick surgical fixes (7 issues): φ/ψ metavariable clarity in the propositional-logic grammar, forward-safe "Sort 0" gloss for Prop, removed "Correction:" labels from citations, more extends/motive/Π-Σ/λ-calculus worked examples and counterexamples.
• Prose-style pass: rewrote dense, jargon-stacked prose and multi-line parentheticals into plain declarative sentences across Chapters 1, 2, 6, 8, 10.
• Full section-number citations: replaced remaining §N shorthand and bare same-chapter "Section N" links with the full "Chapter M, Section N" form, catching two wrong section numbers along the way.
• New categorical diagrams: tikz-cd diagrams for Chapter 1's F-algebra box, Chapter 2's categorical-product and multi-parent-forgetful cases, and Chapter 10's biproduct.

Full details in CHANGELOG v1.4.22.

Includes a source-bundle asset (-source.zip) alongside the PDF, per the usual release format — Markdown, LaTeX, build scripts, and the companion Lean project, all as tracked at this tag.

v1.4.21

See changelog/v1.4.21.md:

• Added a Π vs Σ comparison table to Chapter 1 §5 (notation, generalizes-what, categorical reading, Lean syntax, logic special case, witness-extraction asymmetry).
• Caught and fixed a Pandoc table-rendering bug (empty header cell) along the way.

v1.4.20

See changelog/v1.4.20.md:

• Fixed a rendering bug: a repeated > character leaking into the PDF from Chapter 1 §4's beta-reduction "Programmer's corner" box.
• Fixed a print-unsuitable "The README states..." reference in the same chapter.
• Added a verified worked example to the Motive glossary entry (a genuine "motive is not type correct" failure and its fix).
• Added a second worked example to the Universal property entry (the free-monoid fact from Chapter 1 §1).

v1.4.19

See changelog/v1.4.19.md for the full itemized list:

• Fixed a confusing Nat-overload in two Chapter 1 §3 Vec examples (Vec.replicate/Vec.dot switched to Int with non-sequential values).
• Fixed a stale "Download PDF" badge in the root README (was pinned to v1.4.14).
• Fixed a Π-type family/type conflation and a forward reference to Chapter 3 in Chapter 1 §3.
• Fixed a LaTeX build crash caused by a Pandoc math-span whitespace rule (two instances).