−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).