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.

Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.