Formalising John Dee's Monas Hieroglyphica in Lean 4
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.
Related
- Formalising Linear Elliptic PDE Theory in Lean 4
- John Coates (1945–2022): Celebration of a Life
- Focal Sets of the John Ellipsoid of a Simplex from Its Vertices
- Koebe uniformization, John domains, and transboundary modulus
- Critique of "Use of roster charts in the investigation and prosecution of nurses ..." by John O' Quigley
BibTeX
@misc{matychyn2026formalising,
title = {{Formalising John Dee's Monas Hieroglyphica in Lean 4}},
author = {Ivan Matychyn},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.33104},
eprint = {2610.33104},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.33104},
}
RIS
TY - UNPB
TI - Formalising John Dee's Monas Hieroglyphica in Lean 4
AU - Ivan Matychyn
PY - 2026
DA - 2026/10/22
PB - arXiv
DO - 10.48550/arxiv.2610.33104
UR - https://arxiv.org/abs/2610.33104
AB - 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.
ER -