Rewrite book in derivation-first (Russian-style) prose, v2.0.0 - #251
Open
abderrahim-lectures wants to merge 9 commits into
Open
Rewrite book in derivation-first (Russian-style) prose, v2.0.0#251abderrahim-lectures wants to merge 9 commits into
abderrahim-lectures wants to merge 9 commits into
Conversation
Reverses the v1.5.0 narrative-first direction across every chapter, in the tradition of Arnold's and Gelfand's teaching rather than Bourbaki's: each definition and theorem is derived from the question that forces it, rather than stated and explained afterward. No fixed Definition-Theorem-Proof template is imposed. - Chapter 7 (pilot) and 09-rings/01-definition.md got full body-prose rewrites; every other chapter had its "story of this chapter" narrative opener and answered-inline "Socratic questions" exercises fixed, the two recurring violations found across the book (most body prose was already close to compliant). - Follow-up audit fixed: 05-tactics/02-core-tactics.md (was still a flat tactic catalog), two index-page register deviations (Ch1 Q&A scaffold, Ch3 reassuring aside), and three citation gaps (Ch4 Curry-Howard cross-ref, Ch13 simp confluence, Ch14 Lagrange's theorem). - CONTRIBUTING.md, README.md document the new convention; a "Pedagogical approach" section states it explicitly up front. - Bumped to v2.0.0 (major, not patch: this reverses a stated editorial philosophy book-wide). LaTeX regenerated and rebuilt (xelatex x3 + biber), 301 pages, no new errors. Every Lean/Python code block is byte-identical to before this change except two new lemmas (nat_add_zero, nat_zero_mul) added as exercise solutions and mirrored into lean_project/. lake build passes, 8681 jobs, zero errors. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
learning-paths.md: verified every dependency edge in the chapter graph against the rewritten chapters' actual stated prerequisites (checked Chapters 1-9, 13), all confirmed accurate; added a note that a solid arrow now means the target's derivation assumes the source's question was already answered, not just "read this for background." notation-reference.md: verified every "First appears" citation (20 rows) against the rewritten files, all still accurate since this pass never moved where a notion is introduced; added a cross-link to README.md's Pedagogical approach section. LaTeX regenerated for both (learning-paths.tex, notation-reference.tex). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Ran this repo's 7 review skills (loaded from their actual SKILL.md
files, not paraphrased) against the whole book:
adversarial-book-reviewer, adversarial-maths-reviewer,
notation-consistency-reviewer, category-theory-accuracy-reviewer,
lean-code-auditor, proof-search-analyst, latex-typesetting-reviewer.
3 returned Accept/no findings (maths, lean-code, category-theory). The
other 4 found 5 real, narrow issues, all pre-existing (not introduced
by the style rewrite) except one self-inflicted regression from fixing
another, all fixed here:
- Girard citation gap in 06-rigor-check (admitted inline as
"not yet cited"): added [Girard1972]/[Coquand1986] to
bibliography.md and cited properly.
- Exercise 1 of 09-rings/08-exercises.md named a deliverable
(boolAndOrRing/intAddGroupMod2) that didn't match what the appendix
solution actually builds (bool2CommGroup/bool2Ring); fixed to match.
- Two miscited notation-reference.md rows (∈ claimed Chapter 1, first
genuine use is Chapter 11; ⊆ claimed a Lean form that never occurs
in the book's code).
- 10-ring-theorems/03-theorem-2.md retrofitted a plausible-sounding
but wrong reason for a real tactic failure (conv_lhs actually fails
because it's a Mathlib notation unavailable in this Mathlib-free
chapter, not a goal-navigation mismatch as claimed) - verified by
direct compilation.
- LaTeX: Church1941's bibliography URL overflowed the page margin
(537pt, no break points); added \usepackage{xurl}. Also fixed the
undefined-citation regression this same commit introduced by adding
Girard1972/Coquand1986 to bibliography.md without mirroring them
into lean_book_latex/references.bib.
Verified: lake build 8681 jobs zero errors; full LaTeX rebuild
(build_latex.py + 3x xelatex + biber) 302 pages, zero undefined
references/citations.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
A written review report (reviews/2026-08-15/math-algebra-review.md) claimed three CRITICAL content gaps in Chapters 10-11 (mul_zero_left only in appendix, intZModule undefined in the book, Mat2.ext presented as auto-generated). Verified all three directly against the current lean_book/ source: all three are false. mul_zero_left is proved in the main chapter (10-ring-theorems/03-theorem-2.md:32), intZModule is defined in the book (11-modules/04-submodules.md:51), and 07-matrices.md already discloses Mat2.ext is hand-supplied, not auto-generated. The review agent appears to have trusted stale comments in lean_project/*.lean over the actual current book text. The one real, current issue: those stale .lean comments themselves, which describe gaps that no longer exist and could mislead a future maintainer. Reworded to state the current (correct) situation. No Lean code or book prose changed; lake build still 8681 jobs, zero errors. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Includes the report that contained three false CRITICAL findings (math-algebra-review.md), kept as-is for the audit trail; the actual fix for the root cause (stale .lean comments) was committed separately in 38502d8.
…e rewrite
Ran two fresh adversarial passes (adversarial-book-reviewer,
notation-consistency-reviewer) over the whole book, verified every
finding by hand before fixing:
- CRITICAL: top-level README.md still described the pre-rewrite
narrative style ("Picture it like this" analogies, answered-inline
"Socratic questions") as current; replaced with the actual
derivation-first pedagogical approach, mirrored from
lean_book/README.md.
- HIGH: 09-rings/07-matrices.md's "Mathematical reading" box claimed
`ring` closes the associativity goal, contradicting this book's own
Mathlib-free policy stated 30 lines above in the same section.
- HIGH: notation-reference.md claimed `≃`/`Equiv` first appears in
Chapter 11; it's actually used from Chapter 7 onward in Mathlib
equivalent boxes.
- MEDIUM: 13-working-efficiently/05-structuring-lemmas.md cited
`neg_mul` as a Chapter 10 main-text theorem; it's an exercise,
proved only in the appendix.
- HIGH (style): 03-functions-and-structures/00-index.md stated
currying cold; rewritten to derive it from the type of `add`.
- HIGH (style): 12-path-algebras/01-what-is-a-quiver.md asserted the
quiver definition Bourbaki-style; rewritten to derive it from what a
path needs.
lake build still passes (8681 jobs, zero errors); no Lean code blocks
touched.
05-tactics/04-more-tactics.md previously used a repeated header-then-code-then-explanation template for constructor/cases/ induction/unfold/simp, a relabeled Definition-Theorem-Proof skeleton flagged by the independent adversarial-book-reviewer pass. Rewrote to motivate each tactic from a concrete limitation of the ones already introduced, mirroring 02-core-tactics.md's existing treatment of intro/exact/apply/rw: - constructor, motivated by a goal with two independent parts (P ∧ Q) that intro/exact/apply/rw can't split. - cases, motivated by consuming a disjunction hypothesis that constructor's dual problem leaves unsolved. - induction, motivated by cases's `succ k` branch leaving nothing known about the smaller Nat k. - unfold, motivated by rw needing an equation, which a bare definition like `isZero` doesn't state as one. - simp, moved to the end and reframed as automating exactly what the preceding proofs just did by hand, not dispensed first as a shortcut. Also fixed the chapter index's now-stale section-title link text and a since-removed anchor reference. No Lean code blocks changed, only reordered; `lake build` still passes (8681 jobs, zero errors). Left the Chapter 8/10 theorem-section "Claim / Finding the proof / Mathematical reading / Programmer's corner / Mathlib equivalent" structure untouched: the reviewer flagged its consistent headings as template-like, but "Finding the proof" in each section is genuine, non-formulaic derivation, and the trailing three boxes are the book's explicitly-kept reference material (per README's "Pedagogical approach"), not narrative filler. Forcing arbitrary variation in the headings would trade consistency for no gain in genuine derivation.
Both fixes are traced to real findings from the two independent review passes run against this book's Russian-style rewrite, not hypothetical gaps: - adversarial-book-reviewer/SKILL.md: the Fact-Checker persona missed a same-file contradiction (09-rings/07-matrices.md correctly stated this book has no `ring` tactic available, then 30 lines later a "Mathematical reading" box used `ring` anyway) because the persona's description only named cross-chapter inconsistency. Added same-file contradiction as an explicit CRITICAL attack. Also added a "find every copy" scope note: the review caught lean_book/README.md's pedagogical-approach section but missed that the repo's top-level README.md carries a second, independent copy of the same claims that had gone stale — a root-level doc duplicating in-book claims needs the same scrutiny as the primary source. - notation-consistency-reviewer/SKILL.md: added a requirement to grep-verify every notation-reference.md "First appears: Chapter N" claim against the whole book instead of trusting the row as written (missed `Equiv`/`≃` actually first appearing in Chapter 7's Mathlib equivalent boxes, not Chapter 11 as the table claimed), and a new "provenance of cited lemmas" check requiring `grep` for a lemma's actual `theorem` declaration whenever prose cites it as proved "in Chapter N" — catches a lemma cited as a main-text theorem that is actually only an unsolved exercise, proved solely in the appendix.
Traced to concrete errors made while writing this book, not hypothetical gaps: - adversarial-maths-reviewer/SKILL.md: the Skeptical Referee persona now explicitly checks for a missing bridging step between two individually-true sentences (the exact fault I introduced in the Chapter 7 appendix solution 4 self-review: jumping from "the two projections agree" to "the records are equal" without the connecting step), and requires grep-verifying every "see Chapter X, Section Y" citation against the target's real heading text instead of trusting memory (the exact fault behind the wrong "Section 4 of Chapter 9" cross-reference caught and fixed earlier in this project). - latex-typesetting-reviewer/SKILL.md: the Bibliography row now names the bibliography.md/references.bib dual-file sync gap as a known recurring risk with a concrete diff command, since it caused a broken PDF citation in this project on two separate occasions (documented once already in changelog/v1.6.2.md, then recurred in the v2.0.0 Girard/Coquand citation addition) despite a clean-looking Markdown-only review each time.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #250
Summary
direction to a derivation-first exposition (Arnold/Gelfand tradition):
every definition and theorem is earned through the reasoning that
forces it, not stated then explained. No fixed
Definition-Theorem-Proof template.
09-rings/01-definition.mdgot full body-proserewrites; every other chapter had its narrative opener and
answered-inline exercises fixed (the two recurring violations —
most body prose was already close to compliant).
(
05-tactics/02-core-tactics.md), two minor register deviations, andthree citation gaps.
CONTRIBUTING.md/README.mddocument the convention; new"Pedagogical approach" section states it up front.
book-wide).
Test plan
lake buildinlean_project/: 8681 jobs, zero errors.before this change, except two new lemmas (
nat_add_zero,nat_zero_mul) added as exercise solutions and mirrored intolean_project/LeanProject/Ch15AppendixSolutions.lean.python3 lean_book_latex/build/build_latex.pyregeneratescleanly (114 section files).
xelatex+biber): 301 pages, no newerrors or undefined references introduced by this change.
either way).
number.
including Chapter 7's "Chapter 9, Section 7" reference and
Chapter 8's Theorem 1/2/3 references.
Co-Authored-By: Claude Sonnet 5 noreply@anthropic.com