Document Open Access Logo

Canonical for Automated Theorem Proving in Lean

Authors Chase Norman , Jeremy Avigad

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.14.pdf
  • Filesize: 0.71 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Type theory
Keywords
  • Automated Reasoning
  • Interactive Theorem Proving
  • Dependent Type Theory
  • Inhabitation
  • Unification
  • Program Synthesis
  • Formal Methods

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.14

Author Details

Chase Norman
  • Carnegie Mellon University, Pittsburgh, PA, USA
Jeremy Avigad
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the National Science Foundation Graduate Research Fellowship Program under Grant No. DGE2140739. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

Acknowledgements

Canonical was developed with the direct support of Tesla Zhang, Cheng Zhang, Anna Zhang, Linxuan Ma, Asher Kornfeld, Abdalrhman Mohamed, Yue Yao, and Shubham Barghava.

Supplementary Materials

References

  1. Martin Abadi, Luca Cardelli, P.L. Curien, and Jean-Jacques Levy. Explicit substitutions. Technical Report RR-1176, INRIA, March 1990. Projet PARA. URL: https://inria.hal.science/inria-00075382.
  2. Andreas Abel and Brigitte Pientka. Extensions to Miller’s pattern unification for dependent types and records. Mathematical Structures in Computer Science, 28(7):1262-1300, 2018. URL: https://doi.org/10.1017/S0960129518000158.
  3. Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A theorem-proving system for classical type theory. Journal of Automated Reasoning, 16(3):321-353, June 1996. URL: https://doi.org/10.1007/BF00252180.
  4. Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in Lean 4, 2025. URL: https://arxiv.org/abs/2410.16429.
  5. Clark Barrett, Leilani Hadarean, Tim King, Aina Nötzli, Andrew Reynolds, and Cesare Tinelli. cvc5: A versatile and industrial-strength SMT solver. In International Conference on Computer Aided Verification (CAV), volume 13371 of Lecture Notes in Computer Science, pages 415-442. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_5.
  6. Yves Bertot and Pierre Castran. Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions. Springer Publishing Company, Incorporated, 1st edition, 2010. Google Scholar
  7. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. URL: http://dblp.uni-trier.de/db/series/faia/faia185.html.
  8. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of agda - a functional language with dependent types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 73-78, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
  9. Sally C. Brailsford, Chris N. Potts, and Barbara M. Smith. Constraint satisfaction problems: Algorithms and applications. European Journal of Operational Research, 119(3):557-581, 1999. URL: https://doi.org/10.1016/S0377-2217(98)00364-6.
  10. Kevin Buzzard, Jon Eugster, Alexander Bentkamp, Mohammad Pedramfar, and Patrick Massot. Natural number game. Available at https://adam.math.hhu.de/#/g/leanprover-community/nng4 (2025/03).
  11. Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving (ITP 2023), volume 268 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.9.
  12. Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving (ITP 2024), volume 309 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:20, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.10.
  13. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  14. Lukasz Czajka. A shallow embedding of pure type systems into first-order logic. In Types for Proofs and Programs, 2016. URL: https://api.semanticscholar.org/CorpusID:53242790.
  15. Łukasz Czajka. Practical proof search for Coq by type inhabitation. In Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, pages 28-57, Berlin, Heidelberg, 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-51054-1_3.
  16. Łukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for dependent type theory. Journal of Automated Reasoning, 61(1):423-453, June 2018. URL: https://doi.org/10.1007/s10817-018-9458-4.
  17. N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  18. Kefan Dong and Tengyu Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving. ArXiv, abs/2502.00212, 2025. URL: https://doi.org/10.48550/arXiv.2502.00212.
  19. Gilles Dowek. A complete proof synthesis method for the cube of type systems. Journal of Logic and Computation, 3(3):287-315, June 1993. URL: https://doi.org/10.1093/logcom/3.3.287.
  20. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Higher order unification via explicit substitutions. Information and Computation, 157(1):183-235, 2000. URL: https://doi.org/10.1006/inco.1999.2837.
  21. Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett. SMTCoq: A plug-in for integrating SMT solvers into Coq. In Computer Aided Verification - 29th International Conference, Heidelberg, Germany, July 2017. URL: https://hal.science/hal-01669345.
  22. Warren D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13(2):225-230, 1981. URL: https://doi.org/10.1016/0304-3975(81)90040-2.
  23. Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. Implementing Type Theory in Higher Order Constraint Logic Programming. working paper or preprint, November 2017. URL: https://inria.hal.science/hal-01410567.
  24. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, January 1993. URL: https://doi.org/10.1145/138027.138060.
  25. Gerard P. Huet. The undecidability of unification in third order logic. Information and Control, 22(3):257-267, 1973. URL: https://doi.org/10.1016/S0019-9958(73)90301-X.
  26. G.P. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1(1):27-57, 1975. URL: https://doi.org/10.1016/0304-3975(75)90011-0.
  27. Joe Hurd. First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, pages 56-68, 2003. Google Scholar
  28. Luka Janjić. Program synthesis with dependent types. Master’s thesis, Delft University of Technology, Delft, Netherlands, 2024. Google Scholar
  29. Cezary Kaliszyk and Josef Urban. Hol(y)hammer: Online atp service for hol light. Mathematics in Computer Science, 9(1):5-22, March 2015. URL: https://doi.org/10.1007/s11786-014-0182-0.
  30. Cezary Kaliszyk and Josef Urban. Mizar 40 for mizar 40. Journal of Automated Reasoning, 55(3):245-256, October 2015. URL: https://doi.org/10.1007/s10817-015-9330-8.
  31. Wen Kokke and Wouter Swierstra. Auto in agda. In Ralf Hinze and Janis Voigtländer, editors, Mathematics of Program Construction, pages 276-301, Cham, 2015. Springer International Publishing. Google Scholar
  32. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 1-35, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-39799-8_1.
  33. Jannis Limperg and Asta Halkjaer From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 253-266, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575671.
  34. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover: A frontier model for open-source automated theorem proving, 2025. URL: https://doi.org/10.48550/arXiv.2502.07640.
  35. Fredrik Lindblad and Marcin Benke. A tool for automated theorem proving in Agda. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, pages 154-169, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  36. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  37. Jia Meng and Lawrence C. Paulson. Translating higher-order problems to first-order clauses. Journal of Automated Reasoning, 40(1):35-60, 2008. URL: https://doi.org/10.1007/s10817-007-9085-y.
  38. Jia Meng, Claire Quigley, and Lawrence C. Paulson. Automation for interactive proof: First prototype. Information and Computation, 204(10):1575-1596, 2006. Combining Logical Systems. URL: https://doi.org/10.1016/j.ic.2005.05.010.
  39. Dale Miller. Unification of simply typed lambda-terms as logic programming. In Proceedings of the Eighth International Logic Programming Conference, pages 255-269. MIT Press, 1991. Google Scholar
  40. Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark Barrett. Lean-SMT: An SMT tactic for discharging proof goals in Lean, 2025. URL: https://doi.org/10.48550/arXiv.2505.15796.
  41. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  42. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  43. Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms a generalization of environments. Theoretical Computer Science, 198(1):49-98, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00184-9.
  44. Chase Norman. Canonical. Software, (visited on 2025-09-09). URL: https://github.com/chasenorman/Canonical
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24703
  45. Chase Norman. CanonicalLean. Software, version v4.22.0., (visited on 2025-09-09). URL: https://github.com/chasenorman/CanonicalLean
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24708
  46. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511-540, 2001. URL: https://doi.org/10.1017/S0960129501003322.
  47. Brigitte Pientka. Tabling for higher-order logic programming. In Robert Nieuwenhuis, editor, Automated Deduction - CADE-20, pages 54-68, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11532231_5.
  48. G. Plotkin. Building-in equational theories. In Bernard Metlzner and Donald Michie, editors, Machine Intelligence, volume 7, pages 73-90. Edinburgh University Press, 1972. Google Scholar
  49. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, 1965. URL: https://doi.org/10.1145/321250.321253.
  50. Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. In Pascal Fontaine, editor, Proc. of the 27th CADE, Natal, Brasil, number 11716 in LNAI, pages 495-507. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29436-6_29.
  51. Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Automated Deduction - CADE-15, pages 286-300, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFB0054266.
  52. Lukas Skystedt. A new synthesis tool for Agda. Master’s thesis, Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweeden, 2022. Google Scholar
  53. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean copilot: Large language models as copilots for theorem proving in lean, 2025. URL: https://arxiv.org/abs/2404.12534.
  54. Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. Journal of Automated Reasoning, 66:541-564, 2022. URL: https://doi.org/10.1007/s10817-021-09613-z.
  55. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2.5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems, 2024. URL: https://doi.org/10.48550/arXiv.2410.15700.
  56. Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. In The Thirteenth International Conference on Learning Representations, 2025. URL: https://openreview.net/forum?id=I4YAIwrsXa.
  57. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact