Rewrite book in derivation-first (Russian-style) prose, v2.0.0

.gitignore

@@ -8,3 +8,6 @@ reviews/**/*.log
 reviews/**/*-raw.md
 reviews/**/.counter
 reviews/**/*.report
+
+# graphify tool artifacts (any depth)
+**/graphify-out/

CONTRIBUTING.md

@@ -43,11 +43,28 @@ examples of how past issues were scoped.
 
 The book aims for plain, direct academic language throughout: no
 metaphors, rhetorical questions used as a stylistic device, or casual
-asides. Every type-theory or category-theory term introduced gets a
-formal definition (ideally with a citation — see
-[`lean_book/bibliography.md`](lean_book/bibliography.md)) followed by a
-worked example. If a sentence needs two readings to parse, it's a
-candidate for splitting into two plain sentences.
+asides. If a sentence needs two readings to parse, it's a candidate for
+splitting into two plain sentences.
+
+New or rewritten sections follow a derivation-first exposition, in the
+tradition of Arnold's and Gelfand's teaching rather than Bourbaki's: a
+definition or theorem is not stated and then explained, it is *earned*.
+Pose the question or concrete problem that forces it, walk the chain of
+reasoning that discovers it, and only then name and formalize the result
+— proof and motivation are one continuous argument, not two separated
+blocks. There is no fixed Definition→Theorem→Proof→Remark skeleton to
+fill in; structure follows the logic of the argument. Do not open a
+section or chapter with a narrative "story" framing or a "Picture it like
+this" analogy box in place of doing the derivation. Every type-theory or
+category-theory term still gets a formal definition (ideally with a
+citation — see [`lean_book/bibliography.md`](lean_book/bibliography.md))
+and a worked example; abstract or structural motivation is preferred over
+a contrived real-world scenario. Exercises favor fewer, escalating,
+proof-heavy problems ("Prove that...", "Show that...") over repetitive
+drills, and should not give away their own answer inline — solutions
+belong in `lean_book/15-appendix-solutions/`.
+This is now the style of the whole book; [Chapter 7](lean_book/07-groups/00-index.md)
+is a good reference example if you want to see it applied in full.
 
 ## Lean code
 

README.md

@@ -60,14 +60,32 @@ equivalent.
 
 ## Pedagogical approach
 
+This book teaches by derivation, not by dispensation, in the tradition
+of Arnold's and Gelfand's teaching rather than Bourbaki's. "It is
+impossible to understand an unmotivated definition" (Arnold, *On
+Teaching Mathematics*, 1997): every definition and theorem in this book
+is *earned*. A section poses the question or concrete problem that forces
+a concept, walks the reasoning that discovers it, and only then names
+and formalizes the result, mirroring Gelfand's Moscow seminar method of
+finding the simplest example that captures a phenomenon before finding
+the language to state it generally. There is no fixed
+Definition→Theorem→Proof→Remark skeleton imposed on that reasoning;
+structure follows the logic of the argument, not a template. Formulas
+and theorems are proved before they are used, never handed down as rules
+to memorize. Exercises favor fewer, harder, escalating, proof-heavy
+problems over repetitive drills, and do not give away their own answer;
+solutions live in [15-appendix-solutions/](lean_book/15-appendix-solutions/00-index.md).
+See [CONTRIBUTING.md](CONTRIBUTING.md#book-prose-conventions) for the
+convention as a checklist, and
+[Chapter 7](lean_book/07-groups/00-index.md) for it applied in full.
+
 The book uses several recurring devices, applied consistently across all
 15 chapters (Chapters 0–14):
 
-- **Chapter narratives.** Each chapter opens with a story framing the
-  cognitive journey ahead (remember → understand → apply → analyze →
-  evaluate → create) and a "Learning objectives" box naming the
-  concrete goals of that chapter, and closes with a key-points recap before its
-  exercises.
+- **Chapter openers.** Each chapter's `00-index.md` opens with the
+  derivation-first prose described above and a "Learning objectives"
+  box naming the concrete goals of that chapter, and closes with a
+  key-points recap before its exercises.
 - **Mathematical reading.** Most Lean code blocks are followed by a
   "Mathematical reading" box translating the code into the standard
   notation a working algebraist would recognize from a textbook,
@@ -91,13 +109,8 @@ The book uses several recurring devices, applied consistently across all
   tactic-mode proofs) has no such trace, since there is no multi-step
   computation to show.
 - **Sources, quoted.** Every formally cited term closes its section with
-  a verbatim quote, a precise citation, and a "Picture it like this:"
-  gloss explaining the idea through an everyday analogy, real-world,
-  not just mathematical, rather than a second compressed technical
-  restatement.
-- **Socratic questions.** Each chapter includes reflective "why X, not
-  Y?" questions with their answers, distinct from the recap and the
-  exercises.
+  a verbatim quote and a precise citation, tied directly into the
+  derivation rather than glossed through a separate analogy.
 - **Checkpoint projects.** Two projects, placed after Chapter 6 and
   after Chapter 12, apply material from all preceding chapters to a
   single self-contained construction, each with a self-verification step

lean_book/00-setup/00-index.md

@@ -10,13 +10,22 @@
 - Install the Lean 4 toolchain and configure a working editor.
 - Understand why this book builds everything from scratch instead of importing Mathlib from the start.
 
-## The story of this chapter
-
-Before any theorem is stated, three questions must be answered: *why* Lean,
-*can* you run it, and *why* this book builds everything by hand rather than
-trusting an existing library. Each section below addresses one of them in
-turn — not as abstract philosophy, but as a concrete choice with
-concrete consequences for the rest of the book.
+## What forces the setup
+
+Before any theorem is stated, three questions need settling, each forcing
+the next. Why trust a proof to Lean specifically, rather than to pen and
+paper or to a different proof assistant? Given the answer, how does a
+reader actually get Lean running? And once it runs, why does this book
+build every structure by hand rather than importing an existing library
+that already has them? [Section 1](01-why-lean.md) answers the first
+question by fixing what "verified" means for the rest of the book: a
+proof is correct exactly when it type-checks against the kernel of Lean.
+[Section 2](02-installing-toolchain.md) and [Section 3](03-editor.md)
+answer the second, mechanically: install elan, pin a toolchain, add an
+editor that shows the goal state. [Section 4](04-mathlib-note.md)
+answers the third: building `Group`/`Ring` from scratch exposes every
+field and proof obligation Mathlib would otherwise hide behind its
+typeclass hierarchy, which is the entire point of a first encounter.
 
 ## Sections
 

lean_book/00-setup/04-mathlib-note.md

@@ -26,32 +26,33 @@ the from-scratch constructions of Chapter 12; Mathlib appears only in the
 "Mathlib equivalent" boxes from Chapter 7 onward, and in full starting
 Chapter 14.
 
-**Socratic questions.**
-
-1. *`lean_project` already has Mathlib installed as a dependency (it is
-   what powers the "Mathlib equivalent" boxes from Chapter 7 onward),
-   so why not just import it everywhere from page one, instead of
-   building `Group`/`Ring` from scratch first?* Because the point of this
-   book is not merely to *use* a group in Lean, but to see exactly what a
-   group *is* to Lean, namely every field, every proof obligation, with nothing
-   hidden behind the typeclass hierarchy of someone else. A library saves
-   effort by hiding that machinery, and the purpose of this book is for the
-   reader to see it on a first encounter, not have it hidden.
-2. *`elan` pins one exact Lean version per project via `lean-toolchain`.
-   What would go wrong without that pin, on a machine with several Lean
-   projects at once?* A later toolchain update to one project could
-   silently change how the code of another project elaborates or even fails
-   to compile. The entire point of `lean_project/lean-toolchain` reading
-   `leanprover/lean4:v4.32.2` is that every code block in this book stays
-   reproducible regardless of what else is installed system-wide.
-3. *If this book is Mathlib-free by design through Chapter 12, why does
-   Chapter 7 onward show Mathlib code at all?* Because "built from
-   scratch" and "never shown the real library" are different design
-   choices, and this book only commits to the first. Every hand-built
-   definition from Chapter 7 onward is paired with a labeled preview of
-   its Mathlib counterpart, so that the transition to Mathlib in
-   Chapter 14 is a recognition of material already seen, not a cold
-   start.
+**Three design choices, and why each one is forced.**
+
+`lean_project` already has Mathlib installed as a dependency; that is
+what powers the "Mathlib equivalent" boxes from Chapter 7 onward. Importing
+it everywhere from page one, rather than building `Group`/`Ring` from
+scratch first, would be strictly less work. It would also defeat the
+point. The goal is not merely to *use* a group in Lean, but to see exactly
+what a group *is* to Lean: every field, every proof obligation, with
+nothing hidden behind someone else's typeclass hierarchy. A library saves
+effort by hiding that machinery, and the purpose of this book is for the
+reader to see it on a first encounter, not have it hidden.
+
+`elan` pins one exact Lean version per project via `lean-toolchain`.
+Without that pin, on a machine with several Lean projects at once, a
+later toolchain update to one project could silently change how the code
+of another project elaborates, or stop it compiling at all. Pinning
+`lean_project/lean-toolchain` to `leanprover/lean4:v4.32.2` is what keeps
+every code block in this book reproducible regardless of what else is
+installed system-wide.
+
+Finally, if this book is Mathlib-free by design through Chapter 12, why
+does Chapter 7 onward show Mathlib code at all? Because "built from
+scratch" and "never shown the real library" are different design
+choices, and this book only commits to the first. Every hand-built
+definition from Chapter 7 onward is paired with a labeled preview of its
+Mathlib counterpart, so that the transition to Mathlib in Chapter 14 is a
+recognition of material already seen, not a cold start.
 
 ## Next
 

lean_book/01-basics/00-index.md

@@ -10,35 +10,33 @@
 - Write basic `def`s with implicit arguments.
 - Understand what makes a type *dependent* (via `Fin`/`Vec`).
 
-## The story of this chapter
+## What forces the chapter
 
-Every section below answers one question, and each question is forced by
-the answer to the one before it. It helps to see the whole chain before
-working through it line by line.
+Ordinary languages catch a type error, if at all, at the moment the bad
+line runs, possibly months after it shipped, on a rarely-hit branch. What
+would it take to catch it earlier, for every possible input at once,
+rather than one run at a time? Reading the expression once and deciding
+"what kind of thing is this?" before ever running it, exactly what
+`#check` does and `#eval` does not. [Section 1](01-everything-has-a-type.md)
+draws that line, `#check` a static guarantee, `#eval` a one-off fact, the
+foundation everything else in this book stands on.
 
-1. **What is a type, and why does Lean check it before running anything?**
-   ([Section 1](01-everything-has-a-type.md)) Ordinary languages catch
-   type errors, if at all, at the moment the bad line runs, possibly
-   months after it shipped, on a rarely-hit branch. Lean checks the
-   question "what kind of thing is this?" once, by reading the
-   expression, for every possible input at once. That single idea, that
-   `#check` gives a static guarantee while `#eval` gives a one-off fact, is the
-   foundation everything else in this book stands on.
-2. **Given that types are checked this strictly, how are new ones built,
-   and how does Lean avoid forcing tedious repetition at every call
-   site?** ([Section 2](02-def-let-implicit.md)) `def` and `let` are the
-   two ways to name a term. Implicit arguments (`{α : Type}`) are how a
-   single definition like `identity` serves *every* type at once without
-   being rewritten per type. Nothing here is new machinery yet, just the
-   vocabulary needed to read and write ordinary Lean definitions fluently.
-3. **Is a type always fixed in advance, the way `Nat → Nat` never changes
-   its output type?** ([Section 3](03-dependent-types.md)) No, and this
-   is the single feature that separates a proof assistant from an
-   ordinary typed language. A type can depend on a *value*, not just
-   another type. `Fin n` is a different type for each `n`. The
-   *return type* of a function can change depending on which argument it receives. This
-   is what finally lets a signature say "these two lists must have the
-   same length" and have Lean enforce it, rather than merely hope for it.
+Types checked this strictly still need to be built, and reused, without
+rewriting a definition once per type. `def` and `let` are the two ways to
+name a term; implicit arguments (`{α : Type}`) are how a single
+definition like `identity` serves *every* type at once, without being
+rewritten per type. [Section 2](02-def-let-implicit.md) covers this
+vocabulary, no new machinery yet, just what is needed to read and write
+ordinary Lean definitions fluently.
+
+Is a type always fixed in advance, the way `Nat → Nat` never changes its
+output type? No, and this is the one feature separating a proof
+assistant from an ordinary typed language: a type can depend on a
+*value*, not just another type. `Fin n` is a different type for each
+`n`, and a function's *return type* can change depending on which
+argument it receives, letting a signature say "these two lists must have
+the same length" and have Lean enforce it, rather than merely hope for
+it. [Section 3](03-dependent-types.md) works this out concretely.
 
 That single feature, a type depending on a value, is the hook the next
 chapter picks up directly. `Fin`/`Vec` are dependent types encountered

lean_book/01-basics/04-exercises.md

@@ -8,18 +8,15 @@
 runs. A type is *dependent* when a later type mentions an earlier
 *value* (`Vec α n`, `Fin n`), not merely an earlier type.
 
-**Socratic question.**
-
-1. *The return type of `Vec.replicate` mentions the value of its `Nat` argument. A
-   plain function like `Nat.succ` does not. Is the type of `Nat.succ`,
-   `Nat → Nat`, therefore *not* a Π-type?* It still is. `∀ n : Nat, Nat`
-   is a Π-type whose body happens not to mention the bound variable. Every
-   ordinary function type is a Π-type in the degenerate case. "Dependent"
-   describes the *interesting* instances, not a separate kind of arrow.
-   (The general Π-type pattern this answer leans on gets its full formal
-   treatment in [Chapter 2](../02-terminology-and-coc/00-index.md).)
-
-1. Write `Vec.toList : Vec α n → List α`, converting a length-indexed
+**Exercises.**
+
+1. The return type of `Vec.replicate` mentions the value of its `Nat`
+   argument. A plain function like `Nat.succ` does not. Is the type of
+   `Nat.succ`, `Nat → Nat`, therefore *not* a Π-type? (The general
+   Π-type pattern this question turns on gets its full formal treatment
+   in [Chapter 2](../02-terminology-and-coc/00-index.md).)
+
+2. Write `Vec.toList : Vec α n → List α`, converting a length-indexed
    vector to an ordinary list by forgetting its length. Contrast its type
    with the type of `Vec.replicate` from Section 3. Which one is a genuinely *dependent*
    function (its return type mentions the value of the argument), and which

lean_book/02-terminology-and-coc/00-index.md

@@ -12,29 +12,28 @@
 - State precisely how Π-types, Σ-types, and `Prop` irrelevance fit into
   the underlying calculus of Lean.
 
-## The story of this chapter
+## What forces the terminology
 
 Chapter 1 built `Fin`/`Vec`, concrete dependent types, by example, and
-used several words along the way (`elaborate`, `reduce`, `universal
-property`, ...) informally, trusting they were clear enough from context
-to keep moving. That trust gets repaid here, and the two questions this
-chapter answers are forced directly by what Chapter 1 left open.
-
-1. **Several words just got used informally. What do they actually
-   mean?** ([Section 1](01-terminology.md)) This section is a deliberate
-   pause, not a new topic. It is a glossary of the vocabulary already in
-   use in Chapter 1 and needed again below, defined precisely once
-   instead of re-explained informally every time it recurs.
-2. **The dependent function of `Fin` and the dependent pair-like structure of `Vec`
-   both showed up in Chapter 1. Are they two unrelated tricks, or one
-   idea in two shapes?** ([Section 2](02-pi-sigma-and-coc.md)) One idea.
-   The Π-type (dependent function) and Σ-type (dependent pair) are dual
-   generalizations of `→` and `×`, and together with the proof
-   irrelevance of `Prop` they *are* the calculus of constructions, the one formal
-   system every example since the very first `#check 3` of Chapter 1 has
-   secretly been an instance of.
-
-By the end of this chapter, the informal phrase "everything has a type"
+used words like `elaborate`, `reduce`, and `universal property` informally
+along the way, trusting context to carry the meaning. That trust runs out
+once the logic chapters begin, where loose use of these words would start
+hiding genuine distinctions instead of merely being informal shorthand.
+Fixing precise, working definitions for them, with pointers to where the
+full formal treatment lives, is the entire content of
+[Section 1](01-terminology.md), a deliberate pause rather than a new
+topic.
+
+The dependent function of `Fin` and the dependent pair-like structure of
+`Vec` both appeared in Chapter 1 as two separate tricks. Are they related?
+[Section 2](02-pi-sigma-and-coc.md) shows they are the same idea in two
+shapes: the Π-type (dependent function) and Σ-type (dependent pair) are
+dual generalizations of `→` and `×`, and together with the proof
+irrelevance of `Prop` they *are* the calculus of constructions, the one
+formal system every example since the very first `#check 3` of Chapter 1
+has secretly been an instance of.
+
+By the end of the chapter, the informal phrase "everything has a type"
 from Chapter 1, Section 1 has turned into a precise, named formal system.
 Nothing along the way is optional scaffolding to be forgotten afterward.
 The `∀`/`∃` of Chapter 4, the `Group` structure of Chapter 7, and the