{"id":"arxiv/2610.33104","url":"https://arxiv.org/abs/2610.33104","tags":["math.HO"],"score":0,"title":"Formalising John Dee's Monas Hieroglyphica in Lean 4","domain":"math.HO","source":"arxiv","authors":["Ivan Matychyn"],"reviews":0,"subject":"math.HO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-22","reactions":{}}