Accepted Papers
The list of accepted papers is also available with abstracts.
.- Yousef Alhessi, Sólrún Halla Einarsdóttir, Emily First, George Granberry, Moa Johansson and Nicholas Smallbone. Neuro-Symbolic Lemma Conjecturing (details)
- Guy Axelrod, Moa Johansson and Andrea Silvi. Intrinsic Motivation To Construct Terms In A Dependent Type Theory (details)
- Rashid Barket, Uzma Shafiq, Matthew England and Jürgen Gerhard. Transformers to Predict the Applicability of Symbolic Integration Routines (details)
- Tim Fernando. Between min cost search and least action (details)
- Alexandra Fikiori, Asterios Gkantzounis, Foivos Skarpelos and Petros Stefaneas. On Abstract Logics for Interacting Provers (details)
- Cameron Freer, Alexander Lew, Timothy O'Donnell and Vikash Mansinghka. Autoformalization and autoinformalization via probabilistic reasoning (details)
- Alberto Gandolfi. How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems (details)
- Jonathan Julian Huerta Y Munive. DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant (details)
- Konstantinos Kogkalidis, Orestis Melkonian and Jean-Philippe Bernardy. Structure-Aware Neural Representations of Agda Programs (details)
- Alexei Lisitsa. In search of simplicity: a case study in ML and LLM assisted applications of ATP in mathematics (details)
- Yutaka Nagashima and Daniel Sebastian Goc. Proof By Abduction in Isabelle/HOL (details)
- Bartosz Naskręcki. From Mathematical Theory to Machine Learning: Detecting Symmetry Groups in Crystallographic Tilings (details)
- Steven Obua. Abstraction Logic Is All You Need (details)
- Markus Pantsar. The need for ethical guidelines in mathematical research in the time of generative AI (details)
- Luca Pasetto and Christoph Benzmüller. The Fatio Protocol for Formal Dialogue in Isabelle/HOL (details)
- Job Petrovčič, Sebastian Mežnar and Ljupčo Todorovski. Kernel-level expression generator (details)
- Robin Rawiel and Lukas Niehaus. Reinforcement Learning for Term Rewrite Systems (details)
- Stephan Schulz. Automated Theorem Provers as the Hub of the AI Math Ecosystem (details)
- Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia and Anton Podkopaev. Are LLMs Ready for Software Verification? (details)
- Artjoms Sinkarovs. Correct by Construction Machine Learning (details)
- Gleb Solovev, Nikita Khramov, Andrei Kozyrev and Anton Podkopaev. CoqPilot benchmarking framework (details)
- Irina Starikova. Mathematics and Creative AI (details)
- Laetitia Teodorescu, Guillaume Baudart, Emilio Jesús Gallego Arias and Marc Lelarge. NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving (details)
- Samuel Teuber and Bernhard Beckert. Towards LLM-support for Deductive Verification of Java Programs (details)
- Richard Thompson, Adam Pease, Angelos Toutsios, Roberto Milanese Jr. and Jarrad Singley. Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving (details)
- Jules Viennot, Guillaume Baudart, Emilio Jesús Gallego Arias and Marc Lelarge. MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study (details)
- Huajian Xin. Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover (details)
- Maxim Zyskin. Chessboard covers and AI. (details)