Interactive Theorem Proving

Ask about this topic

Momentum

4 papers in the last four weeks, against 1 the four weeks before. 0.0% of all new papers.

Jul 13Week of Sep 28
View on map

Latest papers 22

All topics
CardsList

  1. Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean

    Sep 30, 2026Jules Viennot, Guillaume Baudart, Marc LelargeAutomated Theorem ProvingEvolutionary Optimization

    IRIF, Universit´e Paris Cit´e, Inria, CNRS · DI ENS, PSL University, Inria

  2. Lean Pool: An AI-Maintained Archive of Formalized Mathematics

    Sep 21, 2026Vasily IlinAI Coding AgentsInteractive Theorem Proving

    University of Washington

  3. Autoformalizing Argumentative Material Inferences

    Sep 15, 2026Xin Quan, Reto Gubelmann, André FreitasLogical ReasoningInteractive Theorem Proving

    1Idiap Research Institute, Switzerland · University of Zurich, Switzerland · Department of Computer Science, University of Manchester, UK

  4. Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)

    Sep 7, 2026Christoph Benzmueller, Daniel KirchnerInteractive Theorem Proving

    University of Bamberg, Bamberg, Germany · Freie Universität Berlin, Berlin, Germany

  5. CAPRI: Contract-Aware Proof Repair for Isabelle

    Aug 13, 2026Jim Woodcock, Gabriel Leite, Augusto Sampaio +1LLM AuditingInteractive Theorem Proving

    Southwest University, China · Aarhus University, Denmark · University of York, UK +2

  6. Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study

    Aug 5, 2026Ahmed Ryan, Md Erfan, Akond Ashfaque Ur Rahman +1LLM EvaluationAutomated Theorem Proving

    University of Alabama, Tuscaloosa, Alabama, USA · Auburn University, Auburn, Alabama, USA

  7. BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

    Jul 30, 2026Ruslan KhrulevAutomated Theorem ProvingInteractive Theorem Proving

    Lomonosov Moscow State University

  8. Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB

    Jul 23, 2026Katharina Engels, Jan Gruteser, Michael LeuschelAutomated Theorem ProvingInteractive Theorem Proving

    Heinrich Heine University Düsseldorf · Faculty of Mathematics and Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universitätsstr. 1, D-40225 Düsseldorf

  9. AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

    Jul 17, 2026Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang +4Automated Theorem ProvingInteractive Theorem Proving

    Nanyang Technological University · Singapore · Imperial College London +5

  10. MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research

    Jul 16, 2026Junjie Zhang, Jiayu Liu, Wenbin Liu +11Multi-Agent LLM SystemsAutomated Theorem Proving

    1State Key Laboratory of Cognitive Intelligence, University of Science and Technology of China · School of Mathematical Sciences, University of Science and Technology of China

  11. TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs

    Jul 13, 2026Burak S. Akbudak, Zeynel A. Uluşan, Can S. Erer +1Automated Theorem ProvingTree Search

    Computer Engineering Department, Bogazici University, Istanbul, Turkey · Computer Engineering Department, Koç University, Istanbul, Turkey · Codeway Studios, Istanbul, Turkey +2

  12. First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

    Jul 12, 2026Christoph Benzmüller, Daniel KirchnerAutomated Theorem ProvingInteractive Theorem Proving

    University of Bamberg, Bamberg, Germany · Freie Universität Berlin, Berlin, Germany

  13. OpenProver: Agentic and Interactive Theorem Proving with Lean 4

    Jul 10, 2026Matěj Kripner, Milan StrakaMulti-Agent LLM SystemsAutomated Theorem Proving

    Charles University, Faculty of Mathematics and Physics, Prague, Czech Republic

  14. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    Jul 8, 2026Eric Jiang, Xiao Liang, Yikai Zhang +16Automated Theorem ProvingInteractive Theorem Proving

    University of California, Los Angeles · 2Lawrence Livermore National Laboratory

  15. Reformalization of the Jordan Curve Theorem

    Jul 2, 2026Simon Guilloud, Sankalp Gambhir, Samuel ChassotInteractive Theorem ProvingAutoformalization

    Ecole Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland.

  16. AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities

    Jun 24, 2026Jimmy Xin, Alex Schneidman, Chris Cummins +3Interactive Theorem ProvingFormal Verification

    Axiom Math · Thinking Machines Lab · Recursive Superintelligence, Inc.

  17. Abduction Prover in Isabelle/HOL

    Jun 3, 2026Yutaka Nagashima, Daniel Sebastian GocAutomated Theorem ProvingAbductive Reasoning

    Institute of Computer Science, the Czech Academy of Sciences, Czechia

  18. Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts

    Jun 2, 2026Yiming Fu, Peixuan Liu, Zichen Wang +1Interactive Theorem ProvingLean Theorem Proving

    Department of Mathematics Southern University of Science and Technology · School of Mathematical Sciences Peking University · Center for Machine Learning Research Peking University

  19. LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

    Jun 2, 2026Po-Nien Kung, Linfeng Song, Dawsen Hwang +10Mathematical Reasoning BenchmarksAutomated Theorem Proving

    Google Cloud AI Research · Google Cloud · Google DeepMind

  20. Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)

    May 26, 2026Christoph Benzmüller, Daniel Kirchner, Luca PasettoLogical ReasoningInteractive Theorem Proving

    Otto-Friedrich-Universität Bamberg, Kapuzinerstraße 16, 96047 Bamberg, Germany · Freie Universität Berlin, Kaiserswerther Str. 16-18, 14195 Berlin, Germany · University of Luxembourg, P. de l’Université 2, 4365 Esch-sur-Alzette, Luxembourg

  21. Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4

    May 25, 2026Austin Shen, Yunong ShiInference-Time SearchAutomated Theorem Proving

    University of Michigan · Amazon Web Services

  22. Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints

    Apr 17, 2026Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens +3Interactive Theorem ProvingAutoformalization

    Department of Computer Science, University of Sheffield, United Kingdom · Department of Informatics, King’s College London, United Kingdom · Department of Computer Science, University of Copenhagen, Denmark