Unit type checker simplifies verifying complex mathematical proofs
Unit: a type checker for dependent type theory
Logic in Computer Science
Summary
Checking complicated mathematical proofs by computer often requires complex tools that do many automatic steps behind the scenes. The authors introduce Unit, a new type checker that keeps verification simple and transparent by avoiding automatic guesswork or hidden steps. This allows users to closely follow and understand each step of the proof check. Unit has successfully verified advanced theories in modern mathematics, showing that simpler systems can still handle deep mathematical ideas.
What this means in practice
- •For software verification teams: Enable transparent checking of complex mathematical properties in software without hidden automation steps.
- •For formal methods engineers: Support building proof assistants with simpler core logic that still verify substantial mathematics clearly.
Authors
Thierry Coquand
Abstract
We present Unit, a type checker for dependent type theory with a module system in the tradition of Automath and a uniform treatment of definitions: two uses of a definition are compared by name and arguments before anything is unfolded, and otherwise the definition declared last is opened. There is no unification, no instance search, no tactics and no unfolding heuristic, so the work of checking can be observed and compared with the informal proof. With Unit we have checked a model of univalent type theory, synthetic algebraic geometry up to Châtelet's theorem, and synthetic Stone duality with its cohomology. These developments show that a small, uniform system supports substantial mathematics, and give concrete reasons to reconsider the complexity routinely accepted in proof assistants.