Skip to content

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

Choose a tag to compare

@abderrahim-lectures abderrahim-lectures released this 01 Aug 18:52
· 36 commits to master since this release
70e1358

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.