Interactive theorem proving is today seeing an explosion of use similar to what computer algebra systems (CASs) saw in the late 1980s. But there is another aspect to mathematics that CASs do not do: reasoning and proofs.

Proof systems come in two flavors: automated (generic ones like Vampire, Z3, and E, as well as model checkers, satisfiability (SAT), and satisfiability modulo theory (SMT) solvers) and interactive (such as Coq, Agda, Lean, Isabelle, and Mizar). The latter are still relatively difficult to use--even relatively straightforward proofs can be tedious. This is where hammers come in: they provide heuristic automation aimed at relieving such tedium.

Somewhat ironically, the power of current hammers relies crucially on machine learning. The search space of proofs is simply too large for any kind of exhaustive search, and no good heuristics have yet been designed by humans. However, the libraries of current systems are large enough that machine learning algorithms seem to be able to do the job fairly well.

The paper provides details on the design of one such hammer for Coq. It first gives an excellent overview of the general problem and the current state of the art for all systems. Other sections cover the type theory handled by the system, the translation from type theory to first-order logic with equality, and the all-important proof reconstruction step. This last step is complex because the proof language of most automated provers is very different than the tactic language of Coq. This is followed by a thorough evaluation of the results, both through systematic testing and some case studies.

The paper is also remarkable for its honesty: not only is a hammer a delicate pile of heuristics, but some parts of the presented translation are unsound. The authors make a solid case that, in practice, this is not an issue. The details are rather technical, so the interested reader should read the paper’s lucid and explicit description.

Anyone interested in how machine learning can be applied to heuristic proof search would benefit from reading the “Related Work” and “Premise Selection” sections. The rest of the paper will be of interest to specialists attempting to build a hammer of their own. The design choices that were made are quite well explained. And, as behooves modern scholarship, the source code is available online.