A name on the wall
In July 2026, a team led by archaeologist Franco Rossi (MIT) reported the decipherment of an eleven-glyph inscription — "Text 19" — in a scribal workshop at Xultun, in the Petén of Guatemala. Closing with cheheen ("so says") and a personal signature, it names Sak Tahn Waax ("White-Chested Fox") — the earliest astronomer-mathematician known by name anywhere in the Americas.
The workshop's plaster walls carry astronomical "microtexts": scratch calculations co-indexing the ritual calendar, the solar year, and the synodic periods of Venus and Mars. The scribe's recurring problem is a least-common-multiple problem — when do distinct cosmic cycles reset together? — and it is exactly the kind of statement a modern proof assistant settles with certainty. This chapter formalizes the core of that matrix in Lean 4.
The periods, and where they align
| Cycle | Days | Meaning |
|---|---|---|
| Tzolk'in | 260 | ritual round (13 × 20) |
| Haab' | 365 | vague solar year (18 × 20 + 5) |
| Venus | 584 | synodic period of Venus |
| Mars | 780 | synodic period of Mars = 3 × 260 |
Stacking the periods by least common multiple gives a ladder of alignment windows:
52 years
8 years
2 Rounds · 104 yr
6 Rounds · 312 yr
Why the grand alignment is exactly six Calendar Rounds
Adding Mars looks like it should blow the number up. It doesn't — and the reason is the prettiest fact in the whole matrix. Since $780 = 3 \times 260$, Mars is three Tzolk'in rounds. A system that already contains the Tzolk'in therefore gains nothing from Mars except a single factor of 3:
Equivalently, the Tzolk'in is absorbed by Mars: any day count that returns Mars to its origin has already returned the Tzolk'in, because $260 \mid 780$. Four cycles collapse to three independent constraints, and the grand return of Earth, Venus, Mars and the ritual matrix to a shared origin takes 113,880 days.
The matrix, as dependent type theory
We model each cycle as a modular type ZMod n, define the alignment windows as
nested Nat.lcm, and prove the two structural theorems: Tzolk'in–Mars absorption,
and the grand alignment divisibility bound.
-- the four periods (days) def tzolkin : ℕ := 260 -- ritual round (13 × 20) def haab : ℕ := 365 -- vague solar year def venus : ℕ := 584 -- Venus synodic period def mars : ℕ := 780 -- Mars synodic period = 3 × 260 -- alignment windows as nested least common multiples def calendarRound : ℕ := Nat.lcm tzolkin haab def cosmicAlign : ℕ := Nat.lcm calendarRound venus def grandAlign : ℕ := Nat.lcm cosmicAlign mars -- scalar values (rfl forces kernel evaluation) theorem calendarRound_eq : calendarRound = 18980 := by rfl theorem cosmicAlign_eq : cosmicAlign = 37960 := by rfl theorem grandAlign_eq : grandAlign = 113880 := by rfl theorem grand_six_rounds : grandAlign = 6 * calendarRound := by rfl -- Mars = 3 × Tzolk'in, so adjoining Mars only triples the window theorem grand_is_triple_cosmic : grandAlign = 3 * cosmicAlign := by rfl -- absorption: any day resetting Mars has already reset the Tzolk'in (260 ∣ 780) theorem tzolkin_mars_absorption (d : ℕ) (h : (d : ZMod mars) = 0) : (d : ZMod tzolkin) = 0 := by have dvd_mars : mars ∣ d := (ZMod.natCast_zmod_eq_zero_iff_dvd d mars).mp h have factor : tzolkin ∣ mars := by decide exact (ZMod.natCast_zmod_eq_zero_iff_dvd d tzolkin).mpr (dvd_trans factor dvd_mars) -- grand alignment: resetting all four cycles ⇒ a multiple of 113,880 days theorem grand_alignment (d : ℕ) (h1 : (d : ZMod tzolkin) = 0) (h2 : (d : ZMod haab) = 0) (h3 : (d : ZMod venus) = 0) (h4 : (d : ZMod mars) = 0) : 113880 ∣ d := by have dt := (ZMod.natCast_zmod_eq_zero_iff_dvd d tzolkin).mp h1 have dh := (ZMod.natCast_zmod_eq_zero_iff_dvd d haab).mp h2 have dv := (ZMod.natCast_zmod_eq_zero_iff_dvd d venus).mp h3 have dm := (ZMod.natCast_zmod_eq_zero_iff_dvd d mars).mp h4 have dcr : calendarRound ∣ d := Nat.lcm_dvd dt dh have dca : cosmicAlign ∣ d := Nat.lcm_dvd dcr dv have dga : grandAlign ∣ d := Nat.lcm_dvd dca dm rwa [grandAlign_eq] at dga
The arithmetic (every rfl value, the divisibility facts) is independently verified by exact-integer computation. The Lean proofs are written to be sound but have not yet been run through the kernel — the lake build against Mathlib is deferred until we have the compute for it. Until it passes, this is a careful formalization, not yet a machine-checked one; it will not be cited as "compiles with zero errors" before it does. Full source: MayaCalendar.lean.
Ethnomathematics, on its own terms
Interactive theorem proving has been aimed almost entirely at modern, Western mathematics. Sak Tahn Waax worked without any of it — charcoal and red oxide on stucco — yet his cycle arithmetic obeys exactly the modular-arithmetic and divisibility laws a proof assistant enforces today. Formalizing it treats the work as what it is: rigorous number theory, not "mysticism" or "folk counting." The point of this chapter is small and exact — one corrected constant, one elegant factor of three — but that is the register the material deserves.
- Rossi, F.D., Stuart, D. & Hurst, H. (2026). The identification and work of an eighth-century Maya mathematician. Antiquity, published online 2026, 1–16 (Cambridge University Press). (First View; volume/issue not yet assigned) doi:10.15184/aqy.2026.10378 · Cambridge Core · PDF (open access)
- Archaeologists decipher the name of a Maya astronomer for the first time. National Geographic, 2026. nationalgeographic.com
- Hidden in a Guatemalan ruin for 1,200 years was the signature of a Maya mathematical genius. ScienceAlert, 13 Jul 2026. sciencealert.com
- DMSE researcher identifies first known Maya scientist. MIT DMSE News, 2026. dmse.mit.edu