Canonical for Automated Theorem Proving in Lean
Logic in Computer Science
2025-09-30 v2
Abstract
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.
Keywords
Cite
@article{arxiv.2504.06239,
title = {Canonical for Automated Theorem Proving in Lean},
author = {Chase Norman and Jeremy Avigad},
journal= {arXiv preprint arXiv:2504.06239},
year = {2025}
}