Formalising John Dee's Monas Hieroglyphica in Lean 4
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2610.33104
curl -X POST /api/v1/records/arxiv/2610.33104/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.33104/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'