# Canonical for Automated Theorem Proving in Lean

Preprint · Chase Norman, Jeremy Avigad

- Archive id: arxiv:2504.06239
- Published: 2025-04-08
- Venue: LIPIcs 352 (2025) 14:1-14:20
- DOI: https://doi.org/10.4230/lipics.itp.2025.14
- arXiv: https://arxiv.org/abs/2504.06239
- Source URL: https://arxiv.org/abs/2504.06239
- PDF: https://arxiv.org/pdf/2504.06239
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.