Sledgehammering Without ATPs

Sledgehammer [18, 3] is a tool for Isabelle/HOL [17] that solves proof goals automatically using external automatic theorem provers (ATPs). “Hammer” systems such as Sledgehammer but also HOL(y)Hammer [12] and CoqHammer [9] are made up of four or five main components [6]:

1. 1.

   The relevance filter (or “premise selector”) heuristically identifies a subset of the available facts (definitions, lemmas, theorems, etc.) as possibly relevant to the current goal. Typically, hundreds of facts can be selected without overwhelming the ATP. Sledgehammer includes three relevance filters: MePo is based on iterative selection [15], MaSh is based on naive Bayes and $k$ nearest neighbors [5], and MeSh combines MePo and MaSh.

2. 2.

   The translation module constructs an ATP problem from the selected facts and the current goal, converting them from the proof assistant’s logic (e.g., Isabelle’s polymorphic higher-order logic) to the ATP’s logic.

3. 3.

   The ATP tries to prove the problem. For Sledgehammer, commonly used ATPs include the first-order superposition prover SPASS [7]; the higher-order superposition provers E [21], Vampire [2], and Zipperposition [20]; the higher-order paramodulation prover Leo-III [19]; and the first-order SMT solvers cvc5 [1], veriT [8], and Z3 [10]. Multiple ATPs are tried in parallel.

4. 4.

   On success, the optional proof minimization module repeatedly invokes the ATP with subsets of the facts referenced in the ATP proof, in an attempt to reduce the number of dependencies and speed up the next step, proof reconstruction.

5. 5.

   Finally, the proof reconstruction module transforms a proof found by an ATP into the proof assistant’s input language (e.g., Isabelle’s Isar [22]). Typically, the structure of the ATP proof is discarded, and a single Isabelle proof method (also called tactic) is invoked with the facts referenced in the ATP proof.

As an example, Sledgehammer might select 1024 facts and translate them, along with the goal, to E’s monomorphic higher-order logic. Then suppose E finds a proof involving three facts: $f_1$, $f_2$, and $f_3$. Minimization reduces this list to two: $f_1$ and $f_3$. Finally, by trial and error, Sledgehammer determines that the proof method simp add: $f_1$ $f_3$ solves the Isabelle goal, so this is suggested to the user. The user can simply click this proof method invocation to insert it into their proof development, and move on to the next goal.

The ATPs’ strength is that they can find their way through hundreds of facts. Nevertheless, it is not uncommon for Sledgehammer to fail on a goal that can be solved by a single parameterless call to auto, Isabelle’s main workhorse. The ATPs, which routinely surprise users with nonobvious proofs, can also be a bottleneck.

This suggests an alternative, ATP-free architecture for hammers:

1. 1.

   The relevance filter works as before, except that it selects at most a few dozen facts, because proof methods tend to scale less well than ATPs.

2. 2.

   A proof method is invoked. The selected facts $f_1,\mathrm{\dots },f_n$ are either introduced into the goal as premises (e.g., using $f_1$ $\mathrm{\dots }$ $f_n$ by auto) or are made available to the proof method via parameters (e.g., by (simp add: $f_1$ $\mathrm{\dots }$ $f_n$)), depending on the method.

3. 3.

   On success, the proof minimization module attempts to reduce the number of facts needed for the proof to speed up the proof method.

We implemented this approach in Sledgehammer, with proof methods complementing the ATPs for proof search. The idea is not completely new. Magnushammer [16], whose relevance filter relies on powerful transformers, has a similar architecture and obtained remarkable results. However, the tool is not readily available, and it requires considerably heavier computational resources than Sledgehammer’s faster and simpler relevance filters.

With our evaluation (Section 4), we try to answer the following research questions: How successful is an ATP-free hammer that relies on fast and simple relevance filtering? How fast are proof methods? How successful are ATP and ATP-free hammers when used in combination? But before we try to answer these questions, we review the implementation in Sledgehammer (Section 2) and study an example interaction with the newly extended tool (Section 3).

Sledgehammer has a generic notion of “prover” with two instances: traditional ATPs [14] and SMT solvers [3]. We have now extended the tool with a third instance: proof methods. The supported proof methods are those that Sledgehammer already used for reconstruction and that do not rely on external tools: algebra, argo, auto, blast, fastforce, force, linarith, meson, metis, order, presburger, satx, and simp. Notably, simp performs simplification using equations as oriented rewrite rules, auto extends simp with general-purpose classical reasoning, and blast is a tableau prover [4].

Thus, our ATP-free hammer is not a brand new hammer; rather, it is integrated in an existing hammer that is already part of the users’ workflow. Our objective is to increase the users’ productivity without requiring them to change their habits.

This tool will be part of the next Isabelle release, which is expected at the end of 2025. We used the results of our empirical evaluation to craft a new default portfolio that runs traditional ATPs, SMT solvers, and proof methods in parallel.

The Khovanskii_Theorem entry of the Archive of Formal Proofs formalizes a theorem in additive combinatorics due to Askold Khovanskii [13]. Among the proof steps is the following:

• have $\mathrm{𝗆𝖺𝗉𝟤}(+)(\mathrm{𝗆𝖺𝗉𝟤}(+)xsys)zs=\mathrm{𝗆𝖺𝗉𝟤}(+)xs(\mathrm{𝗆𝖺𝗉𝟤}(+)yszs)$
   for $xsyszs\mathit{::}({}_{}{}^{\prime }a\mathit{::}\mathrm{𝑎𝑏}\mathrm{\_}\mathrm{𝑠𝑒𝑚𝑖𝑔𝑟𝑜𝑢𝑝}\mathrm{\_}\mathrm{𝑎𝑑𝑑})\mathrm{𝑙𝑖𝑠𝑡}$

In Isabelle, the have command states a new goal within a local proof context, and for specifies universally quantified variables. The goal states that the operation $\mathrm{𝗆𝖺𝗉𝟤}(+)$ is associative for any lists $xs$, $ys$, and $zs$ of elements that form an additive abelian semigroup. The function $\mathrm{𝗆𝖺𝗉𝟤}\mathit{::}({}_{}{}^{\prime }a\Rightarrow {}_{}{}^{\prime }b\Rightarrow {}_{}{}^{\prime }c)\Rightarrow {}_{}{}^{\prime }a\mathrm{𝑙𝑖𝑠𝑡}\Rightarrow {}_{}{}^{\prime }b\mathrm{𝑙𝑖𝑠𝑡}\Rightarrow {}_{}{}^{\prime }c\mathrm{𝑙𝑖𝑠𝑡}$ maps a binary function on the respective elements of two lists. The binary operation $+$ is from the additive abelian semigroup structure.

The first thing an Isabelle user might do to prove this goal is to invoke the try0 command to launch several standard proof methods in parallel. This leads to a timeout with no proof found. Next, the user might try Sledgehammer. When invoked as an ATP hammer, Sledgehammer also times out with no proof found. When invoked as an ATP-free hammer, Sledgehammer finds and outputs the following proof:

• by ($\mathrm{𝗌𝗂𝗆𝗉}\mathrm{𝖺𝖽𝖽}:$ case_prodI2 prod.case_distrib zip_assoc case_prod_app
    map_zip_map map_zip_map2 ab_semigroup_add_class.add_ac(1))

For our evaluation, we used Mirabelle [11, Section 4] to evaluate the ATP and ATP-free hammers on goals originating from different sessions of the Isabelle distribution and the Archive of Formal Proofs. Our objective was to include goals from various areas of mathematics and computer science representing diverse formalization styles. Within a session, the goals were selected at regular intervals, alleviating the issue that consecutive goals tend to be similar. We used the repository revisions 0b46bf0a434f of Isabelle (2025-02-25) and 9dac8e411570 of the Archive of Formal Proofs (2025-02-28). The evaluation was run on a server with an Intel Xeon Silver 4114 CPU and 187 GiB of RAM. The raw evaluation data is available online.¹¹1https://doi.org/10.5281/zenodo.15727890

We first ran a representative external prover with a timeout of 10 seconds, 32 facts, and varying relevance filter configurations on 1000 goals (four sessions with 250 goals each). The aim was to identify the relevance filter that works best for a small number of facts. We found out that with MePo, MaSh, and MeSh, the success rate was respectively 30.1 %, 24.4 %, and 32.4 %. Based on theses results, we decided to use MeSh for the remaining experiments. We selected 5000 goals (20 sessions with 250 goals each).

We described a hammer architecture in which the external ATPs are replaced by the proof assistant’s built-in proof methods. We presented an extension of Sledgehammer that implements this idea. The relevance filter is then directly connected to Isabelle’s built-in proof automation. In this way, goals that, given the right facts, are easy for the built-in automation but too difficult for external ATPs can now be solved. Our empirical evaluation found that the newly extended Sledgehammer has a higher success rate than its predecessor based only on ATPs.

Future work includes the classification of facts. Currently, we treat all facts given to a proof method in the same way, but some methods (e.g., $\mathrm{𝖺𝗎𝗍𝗈}$) work better when the provided facts are classified (e.g., into simplification, introduction, and elimination rules). By integrating fact classification into Sledgehammer, we hope to improve the success rate of proof methods.