⚜ PRINCIPIA ORTHOGONA · Book XIV ← Book XIII · Coherence · Book XVII · The Machine Floor →
Book XIV · opened 2026-09-27 · Mathematical and computational linguistics
LINGUISTICS · MATHEMATICALLINGUISTICS · COMPUTATIONAL

The Language of Mathematics

This corpus has written about words all along: five words for one hole, a double root that was also called degenerate, a numeral that names a count, a holology that names a whole. It has never had one place to ask how mathematics becomes a language, and how a machine reads that language back. This volume is that place.
Methodthe corpus's own pages and Lean, read as linguistic data
every count printed by a script (R24)
Claim typeexposition and audit
no new mathematics
AuthorPablo Nogueira Grossi · G6 LLC
Mathematics is written in two languages at once: a natural language that has been bent into precision, and a formal language that a machine can check. Most errors in this corpus happened where the two meet.

1 · Already in the corpus

This material was scattered across five books before this volume gathered it:

pagewhat it does with language
WP-94 · One Hole, Five Wordsa comparative lexicon: five proof systems, five words for an unfinished step, which are not translations of one another
WP-61 · The Root-Language Sweepa synonymy defect: "double root", "degenerate" and "critical point" used interchangeably, with three of the four affected claims false as written
WP-91 · A Theorem Twenty-Seven Characters Longhow much a short statement can carry
Ch 7 · Maximum Meaningthe Sanskrit grammarians' kāraka analysis, read against AI's semantic networks (Briggs, NASA Ames, 1985)
WP-116 · Akṣapāda Had the Systemthe Nyāya sūtras: inference as a structured utterance
Book XI · What a Numeral Namesthe first lexicon: place value as a naming system, proved unique in Lean
Gallery · Chomskythe grammar hierarchy
VDJ Recombinationa formal grammar in the immune system
Book VIII · ch 13 · Holologythe name for the whole: a coined term and the system it heads
Book XIX · AXLE and the ManualLean as a language: its dialect (ch 2), its layers (ch 3), its addresses (ch 4)
Lean lives elsewhere Formal proof language already has three books: XIX · AXLE and the Manual (the language and its manual), XIII · Coherence (what a verification establishes) and XVII · The Machine Floor (each level bound to its text). This volume does not repeat them. It covers the natural-language side of mathematics, links to those books wherever the two sides meet, and makes its own checks in Python.

2 · Chapters

chtitlesourcestate
1The Grammar of Notation — Chomsky's footnote on paired parentheses, proved in Lean; 6÷2(1+2) has two trees; 11,808 formulas here nest at most 3 deepChomsky 1957; Pullum 2011; J&M 2026live
2How Mathematical Prose Parses — imperatives (38x fewer than arXiv proofs; the recipes are in the Lean), 'orthogonal' as a collective predicate (Lean), ambiguity in bitsTanswell & Inglis; Arambillete & de Groote; Balkır; Corneli et al.; Orth; Fatimalive
3How Many Senses a Word Has — the IJL entry template (C→K→F→U) checked: co-predication must be transitive (Lean), the head sense is not the most frequent (WordNet/SemCor)IJL v3/v4; WordNet 3.0live
4Translation Keys — the operator letters across 822 pages as word clusters: one head sense per key, domain fillers, a colliding U; holology passes the testthe corpus; GCM Institutional Edition (2025)live
5The Machines That Read Us — the corpus's four reading tools as textbook NLP; can a classifier file the pages? 0.68 vs 0.45 baseline, macro-F1 0.39Jurafsky & Martin, 3rd ed. draft (2026)live
6Words That Went Wrong — nine words and numbers the corpus once misused (sorry, degenerate, proved, exactly, there is no, 666, 110, proof, U), each with its repair and a count of usage nowthe corpus; WP-94; WP-61live
refKey Register — generated dictionary of the operator keys C, K, F, U: head sense, key set, fillers by domaintools/key_register.pylive
7Maximum Meaning — the NASA Ames paper on Sanskrit (Briggs 1985): a compressed language, a redundant analysis, 5,040 word orders with one meaningBriggs 1985 (held)live
8Six Lines — Hardy & Wright's proof that √2 is irrational, which Wiedijk said no prover could read, in Lean one sentence per step (49 words, 7 lines)Kahle, Towards the Structure of Mathematical Prooflive
9What Types Decide — Leibniz 1684 to I❤LA: one symbol, many laws; Lean: × commutes on ℕ, not on matrices; this series uses the past tense 21× more than Mathematics in LeanLeibniz; Avigad; Aberdein/Ganesalingam; Ganesalingam & Gowers; Macmillan; I❤LA; Stathopoulos & Teufel; Matsuzaki et al.live
10Where Counting Meets Chance — a primer: a chain of n steps holds with chance pn (14 steps at 95% is worse than a coin flip), a swarm of checkers misses with chance (1−q)n; applied to the Swarm Simulator, where shared intent is exactly 0.416t and the printed contraction bound has no global formNogueira Grossi (Swarm Simulator); Wolframlive
Sources wanted No chapter drawing on a source is written until that source is held and hashed in docs/floor-texts.tsv.

3 · What this volume will not claim