AI for Formal Mathematics

We aim to build AI systems that can understand, create, and verify mathematics in collaboration with people and proof assistants.

Related publications

2026

  1. ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
    ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
    Riyaz Ahuja, Tate Rowney, Jeremy Avigad, and 1 more author
    arXiv, 2026
  2. Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
    Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
    Hita Kambhamettu, Will Crichton, Sean Welleck, and 2 more authors
    arXiv, 2026
  3. DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
    DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
    Tate Rowney, Riyaz Ahuja, Jeremy Avigad, and 1 more author
    2026
    FMCAD 2026
    Code
  4. LeanArchitect: Automating Blueprint Generation for Humans and AI
    LeanArchitect: Automating Blueprint Generation for Humans and AI
    Thomas Zhu, Pietro Monticone, Jeremy Avigad, and 1 more author
    2026
    ITP 2026
    Code
  5. Premise Selection for a Lean Hammer
    Premise Selection for a Lean Hammer
    Thomas Zhu, Joshua Clune, Jeremy Avigad, and 2 more authors
    2026
    ICLR 2026 Oral (Top 1%)
    Code Website

2025

  1. miniCTX: Neural Theorem Proving with (Long-)Contexts
    miniCTX: Neural Theorem Proving with (Long-)Contexts
    Jiewen Hu, Thomas Zhu, and Sean Welleck
    ArXiv, 2025
    ICLR 2025 Oral
  2. ImProver: Agent-Based Automated Proof Optimization
    ImProver: Agent-Based Automated Proof Optimization
    Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, and 1 more author
    2025
    ICLR 2025
  3. Lean-STaR: Learning to Interleave Thinking and Proving
    Lean-STaR: Learning to Interleave Thinking and Proving
    Haohan Lin, Zhiqing Sun, Yiming Yang, and 1 more author
    2025
    ICLR 2025 Spotlight

2024

  1. Llemma: An Open Language Model For Mathematics
    Llemma: An Open Language Model For Mathematics
    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, and 6 more authors
    In International Conference on Learning Representations, 2024
    ICLR 2024

2023

  1. llmstep: LLM proofstep suggestions in Lean
    llmstep: LLM proofstep suggestions in Lean
    Sean Welleck, and Rahul Saha
    In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS’23, 2023
  2. Neural theorem proving tutorial
    Neural theorem proving tutorial
    Sean Welleck
    In IJCAI 2023 Tutorial, 2023
  3. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
    Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, and 6 more authors
    In The Eleventh International Conference on Learning Representations , 2023
    ICLR 2023 Oral

2022

  1. NaturalProver: Grounded Mathematical Proof Generation with Language Models
    NaturalProver: Grounded Mathematical Proof Generation with Language Models
    Sean Welleck, Jiacheng Liu, Ximing Lu, and 2 more authors
    In Advances in Neural Information Processing Systems, 2022

2021

  1. NaturalProofs: Mathematical Theorem Proving in Natural Language
    NaturalProofs: Mathematical Theorem Proving in Natural Language
    Sean Welleck, Jiacheng Liu, Ronan Le Bras, and 3 more authors
    In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1), 2021
    NeurIPS 2021 Oral
  2. Towards Grounded Natural Language Proof Generation
    Towards Grounded Natural Language Proof Generation
    Sean Welleck, Jiacheng Liu, Jesse Michael Han, and 1 more author
    In NeurIPS 2021 Workshop on Math AI for Education: Bridging the Gap Between Research and Smart Education, 2021