← Changelog index

---

v1.4.0 — Socratic questions at the end of every chapter

Added a “Socratic questions” block to every chapter (14 in total), positioned between the existing “Key points” recap and that chapter’s exercises (or, for Chapter 13, as a reflective close to the whole book, right before the pointer to the solutions appendix). These are deliberately a different genre from both neighbors: “Key points” states facts; exercises ask the reader to prove something new; a Socratic question poses a “why does X, not Y?” or “what would break if…?” prompt with its own answer immediately following, aimed at surfacing a plausible misconception before confirming or correcting it — closer to oral-exam questioning than either a recap or a problem set. Each chapter’s three questions are specific to that chapter’s own material (e.g. Chapter 6 asks why the Group axioms split id_left/id_right when intGroup never exercises the difference; Chapter 9 asks why neg_seven closes by rfl when the general neg_one_mul needs five lines for the “same” fact), not a generic template repeated fourteen times.

Caught and fixed two real bugs during this pass:

• A Markdown nested-emphasis bug: two questions wrapped their entire text in *...* and also emphasized one inner word the same way (*...how Lean *finds* an instance...*). CommonMark does not nest identical-delimiter emphasis reliably, and Pandoc’s LaTeX output showed it directly — a stray literal asterisk mid-sentence in the compiled PDF, caught only by actually rendering the page, not by reading the source Markdown. Fixed by dropping the redundant inner emphasis in both places (05-rigor-check/05-exercises.md, 06-groups/07-exercises.md).
• A missing Unicode mapping: one new question’s inline code used ↦ (maps-to), the first use of that character inside a code span anywhere in the book; preamble.tex had no newunicodechar entry for it, so Consolas reported a missing-glyph warning. Added \newunicodechar{↦}{\ensuremath{\mapsto}}.

v1.4.0 — Professional LaTeX styling; retire the old PDF pipeline

• Renamed the top-level LaTeX driver from the generic main.tex to lean-for-working-algebraists.tex, matching the book’s own name.
• Moved learning-paths.tex into the front matter, input right after “About this book” and before Chapter 0 — a reader should see the reading paths before starting, not find them buried in the back matter after every chapter.
• Retired the old Pandoc-direct-to-PDF pipeline entirely: build/build_pdf.py, build/pdf-header.tex, build/pdf-metadata.yaml, and build/lean4.xml are removed (lean4.xml’s keyword lists live on, transcribed into latex/lean-listings.tex). build/build_latex.py is now the book’s only build pipeline. README’s “Building a PDF” section replaced with “Building the LaTeX manuscript,” describing the xelatex+biber compile sequence directly.
• Real title page and back cover, replacing the bare \maketitle: a designed title page (title, subtitle, decorative rules, author, toolchain version) in frontmatter.tex, and a new backmatter.tex with a back-cover-style blurb, highlights, and author line, input at the very end of the document.
• Professional chapter/section styling via titlesec (ruled chapter openings, colored section headings) and running headers/footers via fancyhdr. The book’s recurring boxes (mathreading, progcorner, pblproject) are now colored, bordered tcolorboxes instead of plain amsthm remarks.
• Fixed a real chapter-numbering bug introduced by the styling pass: \thechapter (LaTeX’s automatic counter, incrementing once per \chapter{} call including the unnumbered Appendix) does not line up with the book’s own chapter numbers (Chapter 0 for 00-setup/, etc.), so Chapter 6’s opening page showed both “Chapter 8” (wrong, automatic) and “Chapter 6: …” (correct, from the title text itself) stacked on top of each other. Fixed by dropping the automatic number entirely — every chapter’s title already states its own correct number as prose.
• Fixed a pervasive double-escaping bug: Pandoc’s --listings output already LaTeX-escapes inline code content (`#eval x` becomes \lstinline!\#eval x!, already correctly escaped), but this pipeline’s conversion to \texttt{} was escaping it again, turning every inline-code #, _, and & into a visible literal backslash character (e.g. norm\_num displaying with the backslash showing, instead of rendering as norm_num) — affected essentially every inline code reference in the entire book. Verified directly against Pandoc’s actual output before fixing, not assumed.
• \newtcolorbox’s own optional-argument bracket is reserved for its key=value options and cannot take a plain title string containing a comma (a second real bug, caught immediately since it’s a hard compile error): the checkpoint-project title moved from that bracket to a bold first line inside the box body instead.

v1.4.0 — LaTeX manuscript generation, and a learning-paths page

• Added learning-paths.md: a chapter-dependency graph plus four named reading paths for readers starting from different backgrounds (already know Lean, already know algebra, want the formal foundations first, or want to see Lean prove real theorems as fast as possible), linked from the README and “How to read this book.”
• Added build/build_latex.py, generating a full LaTeX manuscript from the finished Markdown into a new lean_book/latex/ tree — one .tex per Markdown section file (108 in total, mirroring the source layout exactly), a driver per chapter, and a top-level lean-for-working-algebraists.tex. This phase stops at .tex; no PDF is produced by the script itself (a Springer submission wants LaTeX source, not a pre-rendered PDF), though the whole tree was compiled end to end via xelatex+biber repeatedly during development to verify it actually works (219 pages, zero errors, zero missing characters, zero unresolved cross-references in the final pass) — that verification PDF is not committed.
• Every Mermaid diagram hand-translated to native tikz-cd (8 in total: the universal-property/initial-object/forgetful-functor/subobject diagrams in Chapter 1 §4, the product/coproduct diagrams in Chapter 3 §5, the quiver diagram in Chapter 11 §3, and the new chapter-dependency graph), each with its own standalone compile smoke-test in lean_book/latex/smoketest/.
• Consolidated bibliography carried over as references.bib (BibTeX, one entry per bibliography.md source, same keys), cited via \cite{}/biblatex — not a second, hand-maintained copy.
• Custom amsthm environments for the book’s recurring boxes: mathreading (“Mathematical reading”), progcorner (“Programmer’s corner (Python)”), and pblproject (the two checkpoint projects, wrapped whole).
• Lean and Python code via listings, not Pandoc’s default Skylighting output: lean-listings.tex defines a lean language for listings (keywords and tactics carried over from build/lean4.xml, the same syntax definition the PDF-build pipeline uses) and a matching python style, styled identically (font, frame, colors).
• Cross-chapter references ([Chapter 5 §2](../05-rigor-check/...)) become working \hyperref[...]{...} links, not literal prose text — every section gets a unique, hand-assigned label (sec:<chapter>:<file>:<n>) rather than relying on Pandoc’s own auto-slugged labels, which collide across chapters (nearly every chapter has a heading literally titled “Exercises”). Known simplification: links with a #fragment anchor resolve to the file’s first heading, not the exact sub-heading; every such link still lands on the correct section, just not the precise paragraph.
• Real bugs hit and fixed while building the pipeline, each worth noting since they’d recur for any similar Pandoc-fragment-mode LaTeX generation: Pandoc’s \passthrough/\tightlist/\real helper macros are normally supplied by its own --standalone template, which this per-section pipeline doesn’t use, so they’re provided by hand in preamble.tex; \lstinline (used for Pandoc’s inline code spans) breaks on this book’s Unicode math operators even without any other interference, so inline code renders as escaped \texttt{} instead; Pandoc’s longtable+caption output for small lookup tables errored under a caption/longtable counter interaction with no --standalone template to configure it, so tables are simplified to plain tabular; and \input paths are resolved relative to the top-level driver’s own directory, not the including section file’s, which affects every diagram and image reference.
• Do not adopt Springer’s svmult/svmono class files in this pass — a separate, later decision — lean_book/latex/ uses plain, portable LaTeX throughout.

v1.4.0 — Learning objectives, key points, and a consolidated bibliography

• Added a short “Learning objectives” paragraph to every chapter’s 00-index.md (Chapters 0–13), stating what a reader should be able to do by the end of that chapter.
• Added a brief “Key points” recap immediately before each chapter’s exercises (or, for the three chapters without an exercises file — Chapters 0, 2, 12 — at the end of the chapter’s last section). Chapter 13 was left without one, since 01-what-we-built.md already serves as a whole-book recap.
• Consolidated every chapter’s References section into one Bibliography, de-duplicating first: Pierce’s Types and Programming Languages alone was cited in full, with slightly different text, in five different chapters, and several other sources (Dummit & Foote, the Python typing/mypy docs, Milner 1978, the CoC paper, Theorem Proving in Lean 4) were repeated at least once. Every source now has exactly one full citation, on the bibliography page; each chapter’s own References section keeps only a short pointer plus the section-specific reason for citing it. Three sources missed by the original per-chapter passes (Gentzen 1935, Gödel 1930, Martin-Löf 1984) were folded in during this consolidation. Added to the README’s Reference list.
• No Lean code was touched in this pass; lake build on the companion lean_project re-confirmed unaffected.

v1.4.0 — Project-Based Learning components

Distributed PBL scaffolding through the book instead of leaving it only at the very end:

• Added a new checkpoint project at the end of Part I, 05-rigor-check/06-checkpoint-project.md: build a Monoid from scratch (Group minus inverses) and prove identity uniqueness for it, one chapter ahead of Group itself. Full worked solution (with a second instance) added to Appendix, Chapter 5.
• Added a second checkpoint project at the end of Part II, 11-path-algebras/07-checkpoint-project.md: define Path.length and prove Path.append respects it. This surfaced a real, verified fact about Lean worth documenting directly — functions matching on an indexed inductive type like Path reduce only through their equation lemmas (simp only [...]), not plain rfl, once an abstract argument is involved. Full worked solution added to Appendix, Chapter 11; Chapter 13’s “What we built” updated to name this as a second explained exception to the book’s no-simp discipline (alongside Chapter 6’s Perm3.ext), rather than leave the claim overstated.
• Both new chapters’ 00-index.md and their exercises files’ navigation updated to include the checkpoint project as the chapter’s closing section.
• Expanded Chapter 13 §3’s five one-line “suggested next projects” into full scaffolds (learning objectives, prerequisites, milestones, a concrete deliverable, and a self-verification step the reader can run), modeled on §2’s “Two theorems for free” capstone rigor. These remain genuinely open — no appendix solutions were added for them, unlike the two checkpoint projects, since they were never worked exercises with answers in the first place.

v1.4.0 — Full-book review pass (Chapters 2, 4, 6–13, solutions appendix)

Applied the same verification discipline used for the type-theory rewrite (every Lean snippet re-run against the pinned toolchain via lake env lean/lake build; every factual and cross-reference claim checked) to every remaining chapter. Found and fixed several real bugs a read-through alone would have missed:

• Wrong lemma name in a solution. Appendix, Chapter 5’s exercise 1 solution claimed rw [Nat.two_mul] closes n * 2 = n + n; running it fails, since Nat.two_mul : 2 * n = n + n has the arguments in the other order. Fixed to the correct Nat.mul_two : n * 2 = n + n.
• A tool-output claim that didn’t match the real toolchain. Chapter 12 §1 claimed exact? suggests exact h.symm for a simple symmetry goal; run against this book’s pinned toolchain, it instead returns a correct but far less readable term. Rewrote the section to show the verified actual output and make the point honestly (search tactics find a closing term, not necessarily the most idiomatic one).
• A missing exercise solution. Appendix, Chapter 8 had solutions for exercises 1–2 but not 3 (mat2_not_comm), even though the theorem was already proved and verified in the companion Lean project. Added the missing solution and explanation.
• Repeated chapter mislabeling. Chapter 12 attributed the “find the proof by search, not just present the answer” discipline and its multi-step rw/have proofs to “Chapters 6 and 8” in five places across four files; that framing and those proofs are actually in Chapters 7 and 9 (6 and 8 are the definition chapters). Corrected throughout.
• A stale cross-reference. Chapter 10 §5 attributed evenSubmodule to “Chapter 9”; it’s defined earlier in the same chapter, in §4. Fixed to point to §4 directly.
• An overclaim about the book’s own tactic usage. Chapter 13 claimed “there is no simp” anywhere in the book; Chapter 6 §4’s Perm3.ext genuinely uses simp only [mk.injEq], since core Lean generates no field-wise extensionality lemma for a plain structure. Softened the claim and named the one explained exception.
• Added References sections (real, verified sources) to chapters that were missing them despite making external, checkable claims: Chapter 2 (structure-as-product, parametric polymorphism, forgetful functors), Chapter 8 §3 (Dummit & Foote, Aluffi), Chapter 10 §2 (Dummit & Foote, Weibel), and Chapter 11 §5 (Assem–Simson–Skowroński, Schiffler).
• Fixed a stale “first used” location for sorry in the tactic and library reference (claimed Chapter 7; it’s actually introduced in Chapter 4 §3).
• Re-verified every Lean code block in Chapters 6–11 and 13 (both the from-scratch and “Mathlib equivalent” boxes) by rebuilding the entire companion lean_project — including its LeanProjectMathlib modules — against the pinned v4.31.0 toolchain; confirmed every book code block still matches its ported module exactly, with no drift.
• Ran a full site-wide Markdown link-integrity sweep; the only unresolved link is a pre-existing, intentionally preserved historical reference in this changelog (see above, “09-chapter-11.md” predates the Appendix B renumbering).

v1.4.0 — Type-theory chapters rewritten, Appendix B eliminated

• Rewrote Chapter 1 §1 and §3 to lead with concrete, toolchain-verified examples (Fin, Vec/Vec.replicate/Vec.head/ Vec.dot, Sigma, proof irrelevance) and Python-first comparisons before the categorical/formal framing, addressing confusion with the prior dependent-types explanation. Added a References section, citing real, checked sources, to every chapter touched by this pass.
• Eliminated Appendix B entirely, merging its ~9,000 words of formal λ-calculus/CoC material directly into the main chapters that already pointed to it, rather than leaving it as backmatter most readers would skip:
  • The standard-logic recap (natural deduction, soundness/completeness, classical vs. intuitionistic) is now Chapter 3 §2, immediately after the Curry–Howard table that motivates it, renumbering §2-§7 to §3-§8.
  • The untyped λ-calculus recap (grammar, α/β-reduction, currying, Church–Rosser, the $K$ combinator) is woven directly into Chapter 1 §4’s “Reduce/reduction” glossary entry.
  • Π-types, Prop irrelevance, Σ-types, and the CoC/CIC summary are now Chapter 1 §5; the simply typed λ-calculus’s typing judgments/progress/preservation and the universe-formation typing rule are now a new Chapter 5 §3, extending §2’s informal universe discussion.
  • Church encodings (booleans, numerals) became a self-contained aside in Chapter 13, since nothing else in the book depended on them.
  • The λ-calculus/Lean dictionary table is now a standalone reference page, sibling to tactic-and-library-reference.md.
  • Added a new Chapter 1 exercises section (01-basics/06-exercises.md) with solutions, and renumbered the solutions appendix (14-appendix-solutions/) throughout to make room for it.
  • Every cross-reference into this content, in both directions, was rewritten to point at its new home; a full link-integrity sweep across every .md file in the book found zero broken internal links after the 15-lambda-calculus/ directory was removed.