Every century writes its proofs on a different surface.

A scribe pressed number triples into wet clay in Larsa, ~1800 BCE. Alan Oppenheim chalked the convolution integral onto an MIT board in 1987. In 2026, a proof kernel re-reads both — and accepts the mathematics while catching the copying errors. This archive collects historical teaching materials, extracts their claims, and submits them to Lean 4. Clay, chalk, kernel: same discipline, new referee.

c. 1800 BCE Clay stylus · base 60 · Larsa

1987 CE Chalk videotape · MIT 6.003 → OCW

2026 CE Kernel Lean 4 · decide · rfl

Kernel verdicts ✓ kernel-checkedcompiles here, core Lean ◆ in Mathlibalready formalized upstream ⧗ targetgeneral theorem planned ✗ rejected as writtensource contains an error

−1800

Larsa, Mesopotamia

VA-001 · clay

Accession VA-001 · Columbia University, Plimpton Collection

Plimpton 322

Old Babylonian tablet, 15 rows of Pythagorean data in base 60. Column II gives the short side, Column III the diagonal; the long side is left for the reader to reconstruct.

Extracted claim Each row (s, d) admits a natural number l with s² + l² = d². Row 1: 119² + 120² = 169².

Plimpton322.lean · core Lean 4, no Mathlib ✓ kernel-checked✗ rows 9·13·15 as written

def IsPythagoreanTriple (s l d : Nat) : Prop :=
  s * s + l * l = d * d
theorem row_01 : IsPythagoreanTriple 119 120 169 := by decide
-- The scribe's hand slips; the kernel notices, 3,800 years later.
-- Row 9 as written: 541 (9,01) where 481 (8,01) belongs.
example : ¬ IsPythagoreanTriple 541 600 769 := by decide
-- Row 15 as written: diagonal 53 — half the true value 106.
example : ¬ IsPythagoreanTriple 56 90 53 := by decide

English gloss · B1 A clay tablet from ancient Iraq lists special number triples. The computer checks all fifteen rows. The math is correct — but the writer made three copying mistakes, and the computer finds them.

L1 note · PT-BR Aqui, tablet = tabuinha de argila — não o aparelho eletrônico. E diagonal é cognato transparente: pode confiar.

−300

Alexandria

VA-002 · papyrus

Accession VA-002 · Euclid, Elements, Book I

Proposition I.47

The general theorem behind every row of VA-001, stated and proved two millennia later — the square on the hypotenuse equals the sum of the squares on the legs.

Extracted claim In a triangle, the angle at C is right ⇔ dist(A,C)² + dist(B,C)² = dist(A,B)².

Mathlib · Geometry.Euclidean.Angle ◆ in Mathlib

-- Already upstream; the archive cites rather than re-proves.
#check @EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_iff_angle_eq_pi_div_two
-- ∠ A C B = π / 2  ↔  dist A C ^ 2 + dist B C ^ 2 = dist A B ^ 2

English gloss · B1 Euclid proved the general rule for right triangles. Mathematicians have already put this proof inside the computer library, so we point to it — we do not repeat it.

L1 note · PT-BR Right angle = ângulo reto — não "ângulo direito". Em inglês, right tem dois sentidos: "direita" e "correto/reto".

825

Baghdad

VA-003 · paper

Accession VA-003 · al-Khwarizmi, al-Kitab al-mukhtasar fi hisab al-jabr wa'l-muqabala

Completing the square

The book that named algebra solves quadratics by a geometric recipe: build the square, balance the sides. The recipe's engine is one polynomial identity.

Extracted claim x² + bx = (x + b/2)² − b²/4, the identity that reduces every quadratic to a square root.

with Mathlib.Tactic.Ring · rationals ✓ kernel-checked

theorem al_jabr (x b : ℚ) :
    x ^ 2 + b * x = (x + b / 2) ^ 2 - (b / 2) ^ 2 := by ring

English gloss · A2 This old book gives a recipe for solving equations. In Lean, one word — ring — checks the whole recipe.

L1 note · PT-BR Square = quadrado (a forma) e também "elevar ao quadrado" (a operação). O inglês usa a mesma palavra para as duas ideias.

1987

MIT, Cambridge MA

VA-004 · videotape

Accession VA-004 · Oppenheim, RES.6-007 Signals and Systems, Lecture 4

Convolution

Twenty-six chalkboard lectures, taped in 1987 and republished on MIT OpenCourseWare. Lecture 4 builds the convolution sum y[n] = Σ x[k]·h[n−k] and asserts, at the board, that the operation is commutative.

Extracted claim For finite discrete signals, x ∗ h = h ∗ x.

Convolution.lean · core Lean 4, no Mathlib ✓ instances⧗ general theorem

def addZ : List Int → List Int → List Int
  | [], ys => ys
  | xs, [] => xs
  | x :: xs, y :: ys => (x + y) :: addZ xs ys
def conv : List Int → List Int → List Int
  | [], _ => []
  | a :: as, h => addZ (h.map (a * ·)) (0 :: conv as h)
-- Lecture 4's blackboard example, replayed by the kernel:
example : conv [1, 2] [3, 4] = [3, 10, 8] := by decide
-- x ∗ h = h ∗ x — a concrete instance; the ∀ version is the open target.
example : conv [1, 2, 3] [4, 5] = conv [4, 5] [1, 2, 3] := by decide

English gloss · B1 In 1987, a professor filmed his lectures with chalk on a board. He says the order of convolution does not matter. The computer confirms his examples; the full proof for all signals is our next goal.

L1 note · PT-BR Falso amigo clássico: convolution = convolução (operação matemática) — nada a ver com convulsão (convulsion).

2026

TOTOGT

VA-005 · preprint

Accession VA-005 · Grossi, Principia Orthogona Vol. I (non-commutativity theorem) & CatGT — Zeolite Selectivity (empirical instance)

Firing-Order Non-Commutativity

Principia Orthogona, Vol. I formalises the operator chain G = U∘F∘K∘C acting on trajectories in a Riemannian manifold and states Non-Commutativity as one of seven structural theorems (Zenodo, concept DOI 10.5281/zenodo.19117399, V6: 10.5281/zenodo.21146416, July 2026). CatGT, its zeolite-catalysis instantiation (Zenodo, DOI 10.5281/zenodo.21296707), maps this onto a contact 3-manifold X_cat = (r, θ, z) and argues the same four operators (C, K, F, U) explain why HZSM-5 fires C→K→F→U while HMCM-22 fires C→F→K→U — same operators, reversed order, reversed product distribution (Sousa et al.), with the confinement bound r ≤ r*(λ) = √(J/λ) as the accompanying Helical Selectivity Principle.

Extracted claim Theorem 5.3 is exactly an ∃-statement, not a ∀-statement: some valid instances of C, K, F, U are order-dependent (firing order determines the output); other valid instances provably commute. Both are now exhibited on the same manifold.

Theorem53NonCommutativity.lean (TOTOGT/io) + CatGT_Main.lean (TOTOGT/io) · core Lean 4 + Mathlib4 ✓ helical_selectivity (Lean, 0 sorry)✓ thm_5_3_is_exactly_existential (Lean, 0 sorry)

-- Closed in Lean (CatGT_Main.lean) — the confinement bound the HSP rests on:
theorem helical_selectivity (J λ : ℝ) (hJ : 0 < J) (hλ : 0 < λ)
    (r_state : ℝ) (hr : 0 ≤ r_state)
    (h_confined : r_state ^ 2 ≤ J / λ) :
    r_state ≤ criticalRadius J λ hJ hλ := by ...
-- Non-Commutativity (Thm 5.3, Principia Orthogona Vol. I) — isolated into
-- its own file (Theorem53NonCommutativity.lean, TOTOGT/io) so this
-- citation points at something dedicated, not a file buried in the
-- monolithic PrincipiaVol1.lean draft (which has unrelated pre-existing
-- breakage elsewhere -- see that file's own header). Kernel-checked in
-- CI on every push; #print axioms shows only Mathlib's standard axioms
-- (propext, Classical.choice, Quot.sound) on all seven theorems, zero
-- sorryAx:
theorem thm_5_3_is_exactly_existential :
    (∃ M C K F U x, GenerativeOp M C K F U x ≠
      (U.map ∘ K.map ∘ F.map ∘ C.map) x) ∧
    ¬ (∀ M C K F U x, GenerativeOp M C K F U x ≠
      (U.map ∘ K.map ∘ F.map ∘ C.map) x) :=
  ⟨exists_order_dependent, not_forall_order_dependent⟩
-- exists_order_dependent : an explicit instance (shrinkMap/negMap/foldMap
--   on ℤ) where firing order changes the output.
-- not_forall_order_dependent : an explicit instance (an odd fold, foldSym)
--   where two valid operators provably commute -- the ∀-form is false.

English gloss · B1 In a zeolite, a chemical reaction has to happen in a certain order to work. If you do the steps in a different order, the reaction can fail — even though every step is the same. The author wrote a mathematical proof of this idea, and in July 2026 a computer program (a Lean 4 proof checker) confirmed every step of it against pure logic — not just a smaller, related piece, but the full claim itself.

L1 note · PT-BR Commutative = comutativo — quando a ordem não importa (2+3 = 3+2). Non-commutative é o oposto: aqui, a ordem importa porque o sistema tem memória do estado anterior. Aqui, "provado" (pelo autor) e "verificado" (pelo computador, Lean 4) finalmente coincidem — a distinção que esta página costumava marcar já não se aplica a este item.

One schema, any archive.

An accession is not an essay someone must write; it is a record someone (or something) can fill. Five fields, fixed order. The source can be a tablet, a treatise, a videotape, a problem set — anything with a claim inside it.

1 · source

archival material

openly licensed; linked, never rehosted

→

2 · claim

extracted statement

one sentence of mathematics

→

3 · kernel

Lean 4 panel

checked, cited, targeted, or rejected

→

4 · gloss

CEFR English

A2–B2, no simplification of the math

→

5 · L1 note

learner's language

false friends, cognates — PT-BR first

Fields 4 and 5 are where this differs from every formalization gallery: the verification layer and the language layer travel together. Swap the L1 module and the same archive serves Spanish, Mandarin, or Arabic learners — no entry rewritten.