Related papers: The Vampire Diary
We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of…
We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans -- the generation of original…
In this paper, we introduce the concept of a virtual machine with graph-organised memory as a versatile backend for both explicit-state and abstraction-driven verification of software. Our virtual machine uses the LLVM IR as its instruction…
Large language models (LLMs) have been used to generate formal proofs of mathematical theorems in proofs assistants such as Lean. However, we often want to optimize a formal proof with respect to various criteria, depending on its…
Algebraic effects and handlers are a powerful abstraction to build non-local control-flow mechanisms such as resumable exceptions, lightweight threads, co-routines, generators, and asynchronous I/O. All of such features have very evolved…
Answer Set Programming (ASP) is a powerful declarative programming paradigm commonly used for solving challenging search and optimization problems. The modeling languages of ASP are supported by sophisticated solving algorithms (solvers)…
Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may…
Formal verification techniques aim at formally proving the correctness of a computer program with respect to a formal specification, but the expertise and effort required for applying formal specification and verification techniques and…
This paper presents a programming language which includes paradigms that are usually associated with declarative languages, such as sets, rules and search, into an imperative (functional) language. Although these paradigms are separately…
One of the challenging aspects of applying machine learning is the need to identify the algorithms that will perform best for a given dataset. This process can be difficult, time consuming and often requires a great deal of domain…
Earlier work on machine learning for automated reasoning mostly relied on simple, syntactic features combined with sophisticated learning techniques. Using ideas adopted in the software verification community, we propose the investigation…
Computers have already changed the way that humans do mathematics: they enable us to compute efficiently. But will they soon be helping us to reason? And will they one day start reasoning themselves? We give an overview of recent…
AlphaEvolve (Novikov et al., 2025) is a generic evolutionary coding agent that combines the generative capabilities of LLMs with automated evaluation in an iterative evolutionary framework that proposes, tests, and refines algorithmic…
The library \emph{fast\_polynomial} for Sage compiles multivariate polynomials for subsequent fast evaluation. Several evaluation schemes are handled, such as H\"orner, divide and conquer and new ones can be added easily. Notably, a new…
This paper explores the application of automated planning to automated theorem proving, which is a branch of automated reasoning concerned with the development of algorithms and computer programs to construct mathematical proofs. In…
Clause selection is arguably the most important choice point in saturation-based theorem proving. Framing it as a reinforcement learning (RL) task is a way to challenge the human-designed heuristics of state-of-the-art provers and to…
We argue how AI can assist mathematics in three ways: theorem-proving, conjecture formulation, and language processing. Inspired by initial experiments in geometry and theoretical physics in 2017, we summarize how this emerging field has…
Recent developments show that AI can prove research-level theorems in mathematics, both formally and informally. This essay urges mathematicians to stay up-to-date with the technology, to consider the ways it will disrupt mathematical…
Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics…
HolPy is an interactive theorem proving system implemented in Python. It uses higher-order logic as the logical foundation. Its main features include a pervasive use of macros in producing, checking, and storing proofs, a JSON-based format…