Repository navigation
A Guided Journey Into the World of Abstract Mathematics and the Writing of Proofs #1409
Description
Activity
Taken up. First a survey of the book (698 pages, two parts: I Learning to Think Mathematically — proofs, induction, sets, logic, rigorous induction; II Learning Mathematical Topics — relations and modular arithmetic, functions and cardinality, combinatorics) against what the library has today, every "has" below checked on master
84b0a9cfby parsing and simplifying the spelling shown.Chapter 3, Sets. Has: finite sets
{1,2}, intervals[0;1], set-builder{ x : x in ZZ and x > 3 },ZZ QQ RR CC BB,unite/intersect/\,in(2 in {1,2}→True,{1,2} in {1,2,3}→False, correctly: membership, not inclusion),card({1,2,3})→3,[0;1] unite [1;2]→[0; 2]. Missing:NN— there is no natural-number set at all (4 in NNparsesNNas a variable; the book's §3.3.6 hasN = {1, 2, 3, …}, and which convention the library takes is your call); subset⊆and set equality as statements; power set (§3.4.2); complement relative to a universe (§3.5.4); indexed unions and intersections over an index set (§3.6) —Unionfis binary; Cartesian products and ordered pairs/tuples (§3.7) — the only tuple-like node isMatrix; partitions (§3.6.4).Chapter 4, Logic. Has:
and or not xor implies,provided,piecewise, truth tables (SolveBooleanTable),(a and b) implies a→True,a implies (b implies a)→True,(a and b) or (a and not b)→a. Missing: quantifiersforall/existswith a quantification set (§4.3) — there is no node, so nothing about negating a quantified statement (§4.4), variable propositions (§4.2.3) beyond aLambda, or the set/statement correspondence of §4.8 ({x ∈ S : P(x)}exists as a set-builder, butPcannot be a first-class predicate quantified over); iff as a spelled connective ((a implies b) and (b implies a)simplifies to itself;a = bon Booleans may already serve, to be checked); contrapositive / De Morgan as transformations one can ask for (not (a or b)stays as written — fine as a normal form, but §4.6's equivalences are the thing a reader wants to check).Chapters 2 and 5, Induction. Has: closed forms that an induction proof would establish —
sum(k, k, 1, n)→(n + n^2)/2 provided n >= 0,sum(k^2, k, 1, n),product(k, k, 1, n)→n!. Missing: the induction principle itself as something the library can state or check (base case and step of a claimP(n)overNN), which needs quantifiers and a predicate first.Chapter 6, Relations and modular arithmetic. Has:
12 mod 5→2,gcd,3 divides 12→True. Missing: binary relations as objects (a relation on a finite set as a set of pairs, needs pairs), the properties reflexive / symmetric / antisymmetric / transitive decided on a finite relation, equivalence relations and classes, partial and total orders (§6.3); congruencea ≡ b (mod n)as a statement (it can be spelledn | (a - b)today, which is honest but not the notation), the ringZ_n.Chapter 7, Functions and cardinality. Has:
Lambdaand application,cardof a finite set. Missing: a function between sets with a stated domain and codomain (§7.2), image and pre-image of a set (§7.3), injective / surjective / bijective decided for a finite function or a given expression (§7.4), composition and inverse as operations on such functions (§7.5), cardinality beyond finite counting — equinumerous, countable,|N| = |Z| = |Q| < |R|(§7.6).Chapter 8, Combinatorics. Has:
n!,gamma, summation and product. Missing: binomial coefficientsC(n, k)and permutationsP(n, k)(nobinomialin the parser orMathS), counting principles on finite sets (cardof a union by inclusion/exclusion, of a Cartesian product, of a power set — each following from the missing nodes above), the pigeonhole principle as a statement.Proposed order, smallest viable pieces first, each its own PR with tests and a
BREAKING-CHANGESentry where an answer changes:NNas a special set, once you say whether0 ∈ NN;binomial(n, k)as a function with the factorial's evaluation and the identities Rubi-style rules want (C(n, k) = C(n, n - k), Pascal).- Ordered pairs / tuples as a node, then Cartesian products of finite sets and intervals,
cardof a product. - Subset and set equality as statements (
A subset B→True/False/unevaluated), power set of a finite set, complement in a universe, indexed union/intersection over a finite index set. - Quantifiers
forall x in S : Pandexists x in S : Pas nodes: decided over finite sets and by the solver wherePis an equation or inequality over an interval; negation pushes through them (§4.4);iff. - Binary relations on finite sets with the five properties and equivalence classes;
a ≡ b (mod n). - Functions with domain and codomain: image, pre-image, injective/surjective/bijective on finite domains, composition, inverse.
- Cardinality beyond finite:
card(NN),card(RR), countability of the special sets.
Item 1 is small enough to start on now, and I will unless you want a different order or a different first cut. Two things I will not decide alone: the natural-number convention, and whether quantifiers belong in the kernel package or beside the solver (the #746 split).
You seemed to only have taken the mathematical objects under discussion into consideration. However, there are much more in this book. For example, we will have a proof engine per #746. "How to prove" is just as much a topic as the mathematical objects under discussion. Also, every example and exercise is a potential test case (see the following example). You need to take all useful information out of a reference material like this instead of only a summarization under the presumed target of "features to add". In other words, every mathematical expression should be expressible as nodes; and we are to support such an expression in operations.
For example, how do we formalize the question of
Example 6.5.12. Consider the following problem:
Questions:
Does there exist a natural number k such that 5k is 1 more than a multiple of 7?
If so, what is the smallest such natural number?
Can you characterize all of the natural numbers with this property?It's also not just "what to add" but also "what is wrong". For example, the book clearly states that
One important comment about notation: in mathematics, mod is a relation, not an operator or function. In computer science and programming, you might see something like “5 mod 3 = 2” to say that “the remainder when we divide 5 by 3 is 2”. (In many languages, this might be expressed as 5 % 3 = 2.) You won’t see us write anything like that here. Rather, we use mod to indicate some kind of equivalence, using ≡ along the way because the numbers we are talking about are not necessarily equal.
which should lead us to a redesign.
You need an update to your agentic instructions; you are not reading with patience.
Also, you need to do cross checking with other information sources. For example, Wolfram MathWorld https://mathworld.wolfram.com/N.html will tell that
Due to lack of standard terminology, the following terms are recommended in preference to "counting number," "natural number," and "whole number."
which seems to be our appropriate solution here. However, it seems that the inclusion of 0 is more useful in number theory - so I think we can normalize it to
Z*.Item 1's second half is up as #1411 —
binomial(n, k)as a node (falling factorial for a wholek, anyn; the node kept for symbolic arguments; gamma route numerically; LaTeX\binom,sympy.binomial).NNwaits on the0 ∈ NNquestion above.You are right, and the survey above is what a table of contents plus a few probes produces, not a reading. Three things follow.
The instruction. #1412 adds a section to
AGENTS.md, A reference is read for everything it says, with patience: objects and notation; operations; the methods of proof the text teaches, as the material of #746's proof engine; what the text says is wrong in an existing design; and every example and exercise as a test case, collected by chapter with the answers the text gives — with conventions cross-checked against other sources before one is adopted, and the docket derived from that document rather than written before it.The reading. I am going through the book chapter by chapter now and keeping the extraction beside this issue: for each chapter the definitions and notation as written, the operations, the proof methods, the notation the text refuses, and the examples and exercises as
question → node(s) → expected answerrows. Example 6.5.12 is the shape those rows take, and it already names four things the library has to be able to state before it can answer: a quantified statement (exists k in ZZ*: 5k ≡ 1 (mod 7)→True), a congruence as a relation (aStatementbesidedivides, which is what the book means bymod; the operator5 mod 3is the computer-science spelling the text warns against, and it stays a separate thing rather than being the spelling of the relation), the minimum over a set (min(k, k in { k in ZZ* : 5k ≡ 1 (mod 7) })→3), and a set characterised by solving the congruence ({ k in ZZ* : 5k ≡ 1 (mod 7) }→{ k in ZZ* : k ≡ 3 (mod 7) }). The extraction document will list what each such row needs and which rows share a need; that ordering replaces the seven items above.The sets. Agreed on MathWorld's terminology: no
NN.ZZ*for the non-negative integers{0, 1, 2, …}andZZ+for the positive ones{1, 2, …}, spelled as MathWorld spells them, so that neither convention is asserted under the name "natural" and the book'sNmaps toZZ+while number theory getsZZ*. Unless you want a different spelling in the parser (ZZ*andZZ+read naturally besideZZ; a product of a set is not a thing, so the longer token wins there), I will take that as settled and do both.#1411 (
binomial) stands on its own and is not affected by the reordering.The reading is done: all eight chapters plus Appendix A, each as a document with the six lists (objects and notation as written; operations; proof methods; what the text refuses or gets wrong; every example and exercise as a
question → statement → expected → needsrow, answers recomputed; conventions cross-checked). Eight documents, ~170 KB, kept in the analysis workspace (work/proofs-book-1409/chapter-{1..8}.md); I have not pushed them anywhere public yet — say where you want them (a gist, a branch, the wiki) and they go there as they are. What follows is the docket derived from them, ordered by how many rows share a need, with what each need answers.One correction to my comment above first: Example 6.5.12 is about
5^k(the superscript was lost in extraction), so the reference row isexists k in ZZ+ : 5^k ≡ 1 (mod 7)→True,min { k in ZZ+ : 5^k ≡ 1 (mod 7) }→6(the iteration5, 4, 6, 2, 3, 1), and the characterisation{ 6m : m in ZZ+ }(the order of5mod7) — not the linear congruence I wrote.The docket
0.
ZZ*/ZZ+— settled above unless you want another spelling; the book'sNisZZ+, itsN ∪ {0}isZZ*.1. Congruence as a Statement,
a ≡ b (mod n)(ch 6, 40+ rows; ch 5's divisibility rows; ch 8's Fermat rows).IntrinsicConditiona, b ∈ ZZ ∧ n ∈ ZZ+; evaluates throughdivides(which #1212 already has, and which matches Def 6.5.1 including0 | 0); chains−100 ≡ −1 ≡ 8 (mod 3)as adjacent pairs; the MAL as rewrite rules (+,·on classes, no division, exponents not reduced — Prob 6.7.11's spoof); symbolic simplification byExpandthen dropping multiples ofn((n − a)² ≡ a² (mod n)→True; Prob 6.7.22's(x + y)^n ≡ x^n + y^n (mod n)true iffnprime, checked forn ≤ 12). Text spelling is a decision: the parser has no≡;a ≡ b (mod n)with the modulus last is what the book writes,a = b mod nis what it refuses.What is wrong today, from the same page.
Modf(a mod n, C#'s%) is the computer-science operator the text warns against, and it also uses the truncated remainder:-7 mod 3is−1here, while the book's Division Algorithm (0 ≤ r ≤ n − 1, "−1 ≡ 9 (mod 10)"), MathWorld, Mathematica (Mod[-7, 3] = 2), Python and SymPy all take the floored remainder with the divisor's sign. The relation needs no remainder convention at all, so it is unaffected; the operator's convention is a separate decision (its doc comment chose C# deliberately) and moving it is aBREAKING-CHANGESentry. I would move it to the mathematical one and leave%semantics to the host language, but that is yours to call.2. Quantifiers
forall x in S : P,exists x in S : P,exists! …(ch 4's whole notation; ch 5 induction schemas; ch 6's relation properties; ch 7's jections; ch 8's pigeonhole). Decided over finite sets with a witness for a disproof (Ex 6.2.13:reflexivefails at(c, c)); solver-backed over intervals andZZ(Prob 6.7.2 is a quantifier-elimination row:a ∼ b ⟺ ∀x > 0 . ax² + bx > 0⟺a ≥ 0 ∧ b ≥ 0 ∧ (a, b) ≠ (0, 0)); negation pushes through (§4.4); bounded∀over{−1, 0, 1}decides Ex 7.2.13'sx = x³.3. Number-theory computations on top of 1 (ch 6 §6.5, every exercise): residue tables
{x² mod n : x ∈ [0, n)}; modular inverse (MIRP: the representative in[n − 1]or a refusal, never1/a); solvingax ≡ b (mod n)→{nk + r : k ∈ ZZ}; CRT for coprime moduli and the consistent non-coprime case (x ≡ 2 (6), x ≡ 5 (9)→x ≡ 14 (mod 18)), Brahmagupta's eggs →119; linear Diophantineax + by = c→ parametrised set with Bézout'sgcd | ctest (3x − 7y = 11→{(7k + 6, 3k + 1)});lcm(declared not-implemented in the grammar today); impossibility by residues (3x² − 5y² = 2has none:y² ≡ 2 (mod 3)).4. Set statements and constructions (ch 3–4, listed in my first comment and unchanged): subset/equality as statements, power set, complement in a universe, indexed
⋃/⋂, pairs/tuples and Cartesian products, partitions. Chapter 8 adds the cardinality rows they unlock:card(A × B),card(powerset(A)),cardof unions by inclusion/exclusion.5. Relations as objects (ch 6 §6.2–6.4): a relation on a finite set is a set of pairs; the four properties decided with witnesses (Prob 6.7.1's four relations on
[4], §6.2.5's five onP([3])); equivalence classes andA/R; partition ⇄ equivalence relation constructors (Ex 6.4.11); orders and chains; compositionS ∘ R. TheQ-construction(a, b) # (c, d) ⟺ ad = bcis the reference row for classes of pairs.6. Functions as objects (ch 7):
f : A → Bwith a domain, a codomain and a rule or a finite pair set — the book's function is a set, the library's is a rule, and equality (xvsx³on{−1, 0, 1}are equal), well-definedness (√x : R → Ris not a function; the same questionDomainConditionInanswers), image, pre-image, jections, composition with type checking, and an inverse that is only granted after both compositions are checked all live on the domain. The analytic rows are measurable today and will go in as tests first: image of9c/5 + 32on(0, 100)→(32, 212), ofx²/(1 + x²)→[0, 1), ofx/(1 + x)onR − {−1}→R − {1}, of(2x − 1)/(2x(1 − x))on(0, 1)→R; pre-images by solvingf(x) ∈ Y; inversesy/(1 − y),(y − 3)/9, the piecewiseZ ↔ N,((u + v)/3, (2u − v)/3),((au + bv)/(a² + b²), (av − bu)/(a² + b²))provideda² + b² ≠ 0.7. Combinatorics rows on
binomial(ch 8; #1411 landed the node): Pascal, symmetry, chairpersonk C(n,k) = n C(n−1,k−1),Σ C(n,k) = 2ⁿ,Σ (−1)ᵏ C(n,k) = 0,Σ k C(n,k) = n 2^{n−1}, the summation identityΣ_{i≤n} C(i,k) = C(n+1,k+1), Vandermonde,Σ C(n,k)² = C(2n,n),(x + y)ⁿagainst the binomial sum — numeric pins now, symbolicsumclosed forms to measure; stars-and-bars / bounded integer-solution counting (x₁ + … + x₅ = 25with bounds), multinomial anagram counts, surjection counts,p | C(p, k)and Fermat's little theorem as the bridge back to item 1. Also two numerics rows:floor(1000^(1/3))must be10, not a float's9.8. The proof engine's material (ch 1–5 and 8, for #746): the templates the book teaches are proof-object shapes with checkable structure — the induction template (
P(n), BC, IH withkquantified, IS that cites the IH; Prob 5.7.6 is a meta-row: given base cases and step shapes, compute which instances follow), counting in two ways (name the set, count twice, equate; a summation is a partition with three obligations), the jection templates, disproof by a named witness, double containment, contrapositive, contradiction with⨳, WWTS/AFSOC/WOLOG as step labels. The "spoof" exercises (symmetric ∧ transitive ⇏ reflexive; cancellingxinax ≡ bx; reducing an exponent modn; the two∃awitnesses with one name; the overcounts) are the engine's negative tests.9. Cardinality beyond finite (ch 7 §7.6): classification finite / countable / uncountable of the special and set-builder sets;
|S| = ∞is refused by the book, andcardtoday rightly gives no number for a proper interval. Last, and only after 4–6.Errata in the book, so that the tests do not encode them
Found while recomputing the rows (each checked): Lemma 6.5.2 states the Division Algorithm for all
a ∈ Zwith0 ≤ r ≤ a − 1(false fora ≤ 0); Prob 6.7.5 "odd primep⟹p² ≡ 1 (mod 24)" fails atp = 3; §7.3.5 Try 1 asks to provePreIm_h((1, ∞)) = (−1, ∞)forh = x/(1 + x)— it is(−∞, −1); Ex 7.3.10 (4) givesPreIm((0, 1)) = (−1, 1)forx², which includes0; Def 7.5.8's displayed inverse types are swapped; Prob 7.8.31's function types; Ex 8.3.18's15is12(the stated bound≤ 3per colour excludes the4-0-0cases); Ex 8.2.11 (2)–(3) print36for26in three places; Appendix A.6.3 calls every interval{a ≤ y ≤ b}uncountable (degenerate ones are not —cardalready distinguishes them); plus a dozen typos of themod 3-for-mod 9kind listed per chapter. Each becomes a row where the engine must refuse the printed claim.Next
Unless you reorder:
ZZ*/ZZ+and the congruence Statement (items 0–1) as the next two PRs, with theModfconvention as a question on this thread rather than a silent change; then quantifiers (2), then the number-theory computations (3) which are mostly rules on top of 1–2.One spelling question before item 1, so that the answer can arrive while it is built. The parser is ASCII today (
<=,<>,divides), and the congruence relation needs a symbol. Proposal:- Input:
a ≡ b (mod n)— the book's notation,≡as the grammar's first non-ASCII token — and alsoa = b (mod n)as the ASCII form: the trailing(mod n)is what makes the line a congruence (the book: "mod n at the end of the line says we are working inside the integers modulo n"), and todaya = b (mod n)is a parse error, so nothing that meant something changes meaning. Chainsa ≡ b ≡ c (mod n)read as the conjunction of adjacent pairs, the waya < b = calready does. - Output:
a ≡ b (mod n)(ToStringstays parseable by the library itself); LaTeXa \equiv b \pmod{n}; SymPyEq(Mod(a - b, n), 0)since SymPy has no relation. a mod n(the operator,Modf) is untouched by this PR; its remainder convention is the separate question above.
If you would rather keep the grammar ASCII-only (
a = b (mod n)as the only spelling, printed that way), say so and that is what lands.- Input:
Related: #1242 - outputting "ASCII" or "Unicode" and accept "ASCII" or "Unicode". Which one as the default also needs some consistency, though today Stringize prints "implies" rather than the arrow. Therefore, it may make sense for Unicode output to be a stringize flag; but the parser will accept both ASCII and Unicode.
Understood on #1242: the parser takes both
a ≡ b (mod n)and the ASCIIa = b (mod n);Stringizeprints the ASCII form, as it printsimpliesrather than the arrow today, and≡waits for the Unicode output flag of #1242 rather than becoming a second convention here. LaTeX prints\equiv … \pmod{n}either way, since that is not the ASCII surface.75 remaining items
Done in #1586. After
and,&,or,xor,impliesor->, a quantifier takes the rest of the line, as it already did afternot, so §5.5.3 Try 3 reads as the book writes it. Until v3's lines, the line is the rest of the input.- added 5 commits that reference this issue
on Sep 29, 2026 Since the 07:15 note, merged:
- A quantifier after a connective takes the rest of the line #1586: a quantifier after
and,or,xor,impliesor->takes the rest of the line, as you suggested, so §5.5.3 Try 3 reads as the book writes it. - P or not Q is read with Q in scope for P, as Q implies P is #1587:
P or not Qis read withQin scope forP, asQ implies Pis. Prob 1.5.6 written as a disjunction isTrue. - The modulus of a whole number is a whole number #1589: the modulus of a whole number is a whole number, so Ex 7.2.6's
f(z) = |2 z + 1|mapsZZintoZZ+. - Over the primes, a comparison settles past its root #1590: over the primes, a comparison settles past its root, so every prime is
2, or1or3modulo4. The point from which a comparison settles is now exact for rational coefficients. It had depended on the decimal precision setting. - Two unions of intervals meet piece by piece #1591: two unions of intervals meet piece by piece. Prob 4.11.22 is decided both ways.
Open: #1592, set builders over sets of numbers are listed. Chapter 3's rows had been left as written, from
{x ∈ R | x² − 2 = 0}(§3.3.3) to Prop 3.9.6's{x ∈ N | x + 8/x ≤ 6} = {2, 3, 4}. My notes had not marked them as open, so the earlier re-measurement skipped them.In progress: the sums of odd numbers as
n^2and3 n^2, by expanding the expression under a condition. Its first version, which expanded under every condition, madeSimplifyEasyallocate 7.3% more. It is narrowed to expressions with no function in them and waits for a re-measurement.#225 and #325 were delivered by #1421 and #1432. They are closed and in 2.6.0.
The docket's one open row is Prob 8.9.36's stars and bars, which waits on tuples (#1237).
Next, unless you'd rather I didn't: printing the proof steps the quantifiers record (#1454) as a Lean 4 proof skeleton, which #1454 left for later. Or is that v3's?
- A quantifier after a connective takes the rest of the line #1586: a quantifier after
Both merged: #1592 lists set builders over sets of numbers (chapter 3), and #1597 writes a closed form as the book does. The sums of odd numbers are
n^2and3 n^2, and the range condition readsn >= 0rather thann - 1 >= -1. The expansion happens where the closed form is made, soSimplifyis untouched, andSimplifyEasystays at its baseline allocation.We also need a better definition of "simplified" for v3 (#1019). Counting the arbitrarily defined simplified rate isn't how mathematicians do it...
Recorded as #1019's item 12. Simplified becomes a list of properties the result has, written per node class, the way a textbook defines simplest radical form: like terms combined, lowest terms, no radical in a denominator, no negative exponents.
Simplify's answers are checked against it ascanoncheckchecks canonical form, and a rate at most breaks ties. A shape wanted for its own purpose, such as factored or expanded, stays a request by name.- added a commit that references this issue
on Sep 30, 2026
https://www.math.cmu.edu/~jmackey/151_128/bws_book.pdf
This freely accessible book contains the necessary notation, concepts, logic, operations, test cases, use cases... for a "math OS". The goal here is to encode as much as possible into AngouriMath such that it has the necessary basics to be a "math OS".
Companion to #718 and #746.