A Guided Journey Into the World of Abstract Mathematics and the Writing of Proofs

[Happypig375]

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.

[Rafael-SOWNet]

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 84b0a9cf by 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 NN parses NN as a variable; the book's §3.3.6 has N = {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) — Unionf is binary; Cartesian products and ordered pairs/tuples (§3.7) — the only tuple-like node is Matrix; 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: quantifiers forall / exists with a quantification set (§4.3) — there is no node, so nothing about negating a quantified statement (§4.4), variable propositions (§4.2.3) beyond a Lambda, or the set/statement correspondence of §4.8 ({x ∈ S : P(x)} exists as a set-builder, but P cannot be a first-class predicate quantified over); iff as a spelled connective ((a implies b) and (b implies a) simplifies to itself; a = b on 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 claim P(n) over NN), 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); congruence a ≡ b (mod n) as a statement (it can be spelled n | (a - b) today, which is honest but not the notation), the ring Z_n.

Chapter 7, Functions and cardinality. Has: Lambda and application, card of 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 coefficients C(n, k) and permutations P(n, k) (no binomial in the parser or MathS), counting principles on finite sets (card of 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-CHANGES entry where an answer changes:

1. NN as a special set, once you say whether 0 ∈ 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).
2. Ordered pairs / tuples as a node, then Cartesian products of finite sets and intervals, card of a product.
3. 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.
4. Quantifiers forall x in S : P and exists x in S : P as nodes: decided over finite sets and by the solver where P is an equation or inequality over an interval; negation pushes through them (§4.4); iff.
5. Binary relations on finite sets with the five properties and equivalence classes; a ≡ b (mod n).
6. Functions with domain and codomain: image, pre-image, injective/surjective/bijective on finite domains, composition, inverse.
7. 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).

[Happypig375]

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*.

[Rafael-SOWNet]

Item 1's second half is up as #1411 — binomial(n, k) as a node (falling factorial for a whole k, any n; the node kept for symbolic arguments; gamma route numerically; LaTeX \binom, sympy.binomial). NN waits on the 0 ∈ NN question above.

[Rafael-SOWNet]

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 answer rows. 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 (a Statement beside divides, which is what the book means by mod; the operator 5 mod 3 is 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, …} and ZZ+ for the positive ones {1, 2, …}, spelled as MathWorld spells them, so that neither convention is asserted under the name "natural" and the book's N maps to ZZ+ while number theory gets ZZ*. Unless you want a different spelling in the parser (ZZ* and ZZ+ read naturally beside ZZ; 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.

[Rafael-SOWNet]

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 → needs row, 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 is exists k in ZZ+ : 5^k ≡ 1 (mod 7) → True, min { k in ZZ+ : 5^k ≡ 1 (mod 7) } → 6 (the iteration 5, 4, 6, 2, 3, 1), and the characterisation { 6m : m in ZZ+ } (the order of 5 mod 7) — not the linear congruence I wrote.

The docket

0. ZZ* / ZZ+ — settled above unless you want another spelling; the book's N is ZZ+, its N ∪ {0} is ZZ*.

1. Congruence as a Statement, a ≡ b (mod n) (ch 6, 40+ rows; ch 5's divisibility rows; ch 8's Fermat rows). IntrinsicCondition a, b ∈ ZZ ∧ n ∈ ZZ+; evaluates through divides (which #1212 already has, and which matches Def 6.5.1 including 0 | 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 by Expand then dropping multiples of n ((n − a)² ≡ a² (mod n) → True; Prob 6.7.22's (x + y)^n ≡ x^n + y^n (mod n) true iff n prime, checked for n ≤ 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 n is 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 3 is −1 here, 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 a BREAKING-CHANGES entry. 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: reflexive fails at (c, c)); solver-backed over intervals and ZZ (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's x = 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, never 1/a); solving ax ≡ 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 Diophantine ax + by = c → parametrised set with Bézout's gcd | c test (3x − 7y = 11 → {(7k + 6, 3k + 1)}); lcm (declared not-implemented in the grammar today); impossibility by residues (3x² − 5y² = 2 has 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)), card of 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 on P([3])); equivalence classes and A/R; partition ⇄ equivalence relation constructors (Ex 6.4.11); orders and chains; composition S ∘ R. The Q-construction (a, b) # (c, d) ⟺ ad = bc is the reference row for classes of pairs.

6. Functions as objects (ch 7): f : A → B with 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 (x vs x³ on {−1, 0, 1} are equal), well-definedness (√x : R → R is not a function; the same question DomainConditionIn answers), 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 of 9c/5 + 32 on (0, 100) → (32, 212), of x²/(1 + x²) → [0, 1), of x/(1 + x) on R − {−1} → R − {1}, of (2x − 1)/(2x(1 − x)) on (0, 1) → R; pre-images by solving f(x) ∈ Y; inverses y/(1 − y), (y − 3)/9, the piecewise Z ↔ N, ((u + v)/3, (2u − v)/3), ((au + bv)/(a² + b²), (av − bu)/(a² + b²)) provided a² + b² ≠ 0.

7. Combinatorics rows on binomial (ch 8; #1411 landed the node): Pascal, symmetry, chairperson k 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, symbolic sum closed forms to measure; stars-and-bars / bounded integer-solution counting (x₁ + … + x₅ = 25 with 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 be 10, not a float's 9.

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 with k quantified, 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; cancelling x in ax ≡ bx; reducing an exponent mod n; the two ∃a witnesses 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, and card today 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 ∈ Z with 0 ≤ r ≤ a − 1 (false for a ≤ 0); Prob 6.7.5 "odd prime p ⟹ p² ≡ 1 (mod 24)" fails at p = 3; §7.3.5 Try 1 asks to prove PreIm_h((1, ∞)) = (−1, ∞) for h = x/(1 + x) — it is (−∞, −1); Ex 7.3.10 (4) gives PreIm((0, 1)) = (−1, 1) for x², which includes 0; Def 7.5.8's displayed inverse types are swapped; Prob 7.8.31's function types; Ex 8.3.18's 15 is 12 (the stated bound ≤ 3 per colour excludes the 4-0-0 cases); Ex 8.2.11 (2)–(3) print 36 for 26 in three places; Appendix A.6.3 calls every interval {a ≤ y ≤ b} uncountable (degenerate ones are not — card already distinguishes them); plus a dozen typos of the mod 3-for-mod 9 kind 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 the Modf convention 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.

[Rafael-SOWNet]

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 also a = 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 today a = b (mod n) is a parse error, so nothing that meant something changes meaning. Chains a ≡ b ≡ c (mod n) read as the conjunction of adjacent pairs, the way a < b = c already does.
• Output: a ≡ b (mod n) (ToString stays parseable by the library itself); LaTeX a \equiv b \pmod{n}; SymPy Eq(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.

[Happypig375]

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.

[Rafael-SOWNet]

Understood on #1242: the parser takes both a ≡ b (mod n) and the ASCII a = b (mod n); Stringize prints the ASCII form, as it prints implies rather 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.