LEAN · FORMAL VERIFICATION
Lean is a proof assistant: it checks reasoning, step by step, against stated axioms. At SGDL we treat Lean as a tool for empowerment — a way to give verifiability to reasoning about physical space, with the authorship and the trace kept visible. Not an opaque oracle that returns an answer no one can retrace.
Machines now produce more proofs than mathematicians can read. The question is no longer only whether a result is true, but why it is true, and who can retrace it. A result without a trace breaks the scientific practice of crediting the reasoning, not only the answer.
Lean, for us, is high-value but low-level work: making sure that creative efforts — a design, a model, a scientific claim — are guaranteed in some provable way to hold. We aim to be part of a verifiable backbone, the way statistics underwrite an experiment: present, sober, checkable, in support of the effort to understand the world and its physical laws.
Everything on this page is one thing: the Arithmetics of Forms itself (Rotgé, Université de Montréal, 1997), formalized in Lean 4 wall to wall. 1,962 kernel theorems — the inventory’s Part I, drawn from the thesis, the articles and the patents — verified by Lean 4 and Mathlib, re-verifiable by a single compilation command. The applications built on this kernel are counted separately, and are not shown here.
At the root is a single idea. Every point of space is interior, frontier or exterior — a ternary verdict, INT / FRO / EXT. Solids are not meshes; they are written, and they combine by taking the minimum or the maximum of this ternary density. The verdict is exact — decided on the rationals — and it needs no coordinates chosen in advance.
Glue two solids together along an edge, or at a single point, and a mesh representation breaks: at the junction a point has no disk-shaped neighbourhood — it is non-manifold, and an ordinary in / out test becomes undecided. The density verdict assumes no manifold. Because solids combine by minimum and maximum, the junction stays exactly classified — frontier is frontier, interior is interior — where a mesh would simply tear.
This is a property of the density algebra itself, not a special case: no manifold is assumed anywhere, and the verdict at the junction is proven, line by line, in the kernel.
The kernel carries a lineage. Desargues and Pascal gave projective geometry its theorems; Rotgé’s Arithmetics of Forms (1997) made the writing of exact solids algebraic. Lean now checks the whole chain, line by line.
We are integrating a patent portfolio of formal methods for reasoning over space into Lean libraries, so they can be reused by more and more verifiability tools and agentic tools — each result carrying its own re-verifiable trace.
These methods were built to support humans under heavy constraints — understanding and manipulating the world in complex environments, from a space station to a planetary rover. Made formal under Lean, that same expertise can radiate into other fields: medical imaging, the scientifically grounded use of natural resources, earth planning. One exact geometry, verifiable, reused.
