Formalising John Dee's Monas Hieroglyphica in Lean 4
Ivan Matychyn
math.HO
Oct 22, 2026 · v1
TL;DR
Formalises the theorems of John Dee's Monas Hieroglyphica in Lean 4 core (no Mathlib), including a constructive proof that the cube root of 2 is irrational.
Abstract
John Dee's Monas Hieroglyphica (Antwerp, 1564) contains twenty-four numbered theorems about a single composite alchemical glyph, presented in the manner of Euclid: theorem, demonstration, corollary. In this note the following question is considered: which of Dee's theorems can be stated precisely in a proof assistant, and which of them can then be proved? Working in Lean 4 (v4.35.0) with the core library only (without Mathlib), we divide the treatise into three layers: the syntax of the glyph, encoded as inductive data; Dee's arithmetic, verified by kernel computation; and the geometry of the final theorems, in connection with which we prove a classical result not stated by Dee: no ratio of whole numbers doubles the cube, that is, the cube root of two is irrational (the Delian obstruction). The accompanying file Monas.lean compiles with no errors and no sorry. Two observations are made. The cabalistic computation of Theorem XVII, according to which the Cross, "by the best kabbalistic computation," signifies the number 252, is verified, and its proof depends on no axioms: it is a pure computation. The only theorem of the formalisation with genuine mathematical content, the Delian obstruction, is proved constructively and depends only on the axioms propext and Quot.sound.
Problem
John Dee's 1564 Monas Hieroglyphica presents twenty-four Euclid-style theorems about an alchemical glyph. The question is which of these theorems can be stated precisely in a proof assistant, and which of those can then be proved.
Approach
Using Lean 4 (v4.35.0) with only the core library, the treatise is split into three layers. In the first, the glyph's syntax is encoded as an inductive type, with compositional claims proved by rfl or simp. In the second, Dee's arithmetic and numerology identities are checked by the kernel using decide. In the third, motivated by a reading that links the final proportions to doubling the cube, a result Dee did not state is proved: that p^3 = 2q^3 has no solution with q nonzero, by infinite descent using omega and ac_rfl.
Results
Monas.lean (324 lines) compiles with no errors, warnings, or sorry. The 252 computation of Theorem XVII depends on no axioms. The irrationality of the cube root of 2 is proved constructively, depending only on propext and Quot.sound.
| Theorem(s) | Content | Status |
|---|
| VIII | tetraktys; X is the 21st letter | verified arithmetic |
| XI | Aries is two semicircles | definitional (rfl) |
| XII | planetary signs from Moon, Sun, Elements, Aries | verified (computation) |
| XIV | the magistery depends on Sun and Moon | not formalised (alchemical) |
| XVII | the Cross signifies 252 | verified arithmetic (no axioms) |
Status of selected theorems in Monas.lean
