# Canonical for Automated Theorem Proving in Lean

arXiv: https://arxiv.org/abs/2504.06239 · HTML: https://mlsanity.com/paper/2504.06239/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Apr 2025.

## Built on by (most cited first, 2 of 2)

- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [Agentic Proving for Program Verification](https://mlsanity.com/paper/2605.23772/) (2026)

## Abstract (arXiv)

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.