## Stream: general

### Topic: hammers

#### Kevin Buzzard (Apr 23 2020 at 11:26):

I want to write a couple of sentences on "hammers" in general, in an article. Am I right in thinking that the original hammer was sledgehammer, which is something to do with Paulson and/or @Jasmin Blanchette ? Is there something explicit I can cite? This is 2010, right? I googled around but keep finding instruction manuals. Is there a publication for "Hammer for Coq"? I can't find anything other than preprints. Are there hammers for other systems? I know about @Gabriel Ebner 's work in Lean (and I am assuming there is also nothing to cite here). By a hammer I think I mean an interface which enables an ITP to talk to an ATP. Would it be right to claim that hammers are currently any kind of "hot topic" or "active area of study"? Or is the basic idea completely understood and the only issue is what parameters and lemmas one should pass to the ATP? Is the latter question a boring one, basically understood, or something which one could envisage AI having a say in?

#### Rob Lewis (Apr 23 2020 at 11:38):

This paper is a nice early summary and cites the earliest hammer papers at the beginning: https://www.cl.cam.ac.uk/~lp15/papers/Automation/paar.pdf

Jasmin is responsible for some big improvements, including https://people.mpi-inf.mpg.de/~jblanche/enc_types_paper.pdf, but he can better point you to his canonical references.

I think the CoqHammer publication is in JAR, https://link.springer.com/article/10.1007/s10817-018-9458-4

#### Rob Lewis (Apr 23 2020 at 11:39):

Would it be right to claim that hammers are currently any kind of "hot topic" or "active area of study"?

Not really, I'd say. Adapting them for more complicated logics (like CoqHammer) is interesting, but IMO it isn't a "hot topic."

#### Rob Lewis (Apr 23 2020 at 11:41):

the only issue is what parameters and lemmas one should pass to the ATP? Is the latter question a boring one, basically understood, or something which one could envisage AI having a say in?

(This is just my impression, I don't have citations to back this up.) I think relevance filtering is well understood, and it's not really the bottleneck in hammer performance. You can make small gains with fancy AI filters. The bigger bottlenecks are the translations, especially for CIC, ATP performance, and reconstruction.

#### Jasmin Blanchette (Apr 23 2020 at 11:41):

The reference I use for "hammers" is "Hammering towards QED":
https://people.mpi-inf.mpg.de/~jblanche/h4qed.pdf
Its four authors can be considered the main hammer people (Sledgehammer, $\mathrm{Miz}\mathbb{AR}$, HOLyHammer, CoqHammer).

#### Jasmin Blanchette (Apr 23 2020 at 11:41):

(If you go to DBLP (dblp.org), you can look up all the refs I'll give you.)

#### Kevin Buzzard (Apr 23 2020 at 11:42):

Aah super. I was using math reviews which has some stuff (e.g. it had the Coq ring paper), but not all stuff.

#### Jasmin Blanchette (Apr 23 2020 at 11:42):

The PAAR 2010 paper Rob mentioned and the slightly updated IWIL 2010 paper is a good early reference that still gets cited a lot, probably because it has "Sledgehammer" in its title.

#### Jasmin Blanchette (Apr 23 2020 at 11:44):

The "Hammering towards QED" will give you references to all the other systems, including MizAR, as of 2014--2015, though.

#### Kevin Buzzard (Apr 23 2020 at 11:44):

What system is HOLyhammer?

#### Jasmin Blanchette (Apr 23 2020 at 11:44):

It's for HOL Light and HOL4.

#### Jasmin Blanchette (Apr 23 2020 at 11:44):

By Kaliszyk and Urban.

#### Kevin Buzzard (Apr 23 2020 at 11:44):

Is Sledgehammer for Isabelle, or Isabelle/HOL?

/HOL.

#### Kevin Buzzard (Apr 23 2020 at 11:45):

Many thanks Jasmin.

#### Jasmin Blanchette (Apr 23 2020 at 11:45):

There were plans to port it to set theory.

#### Jasmin Blanchette (Apr 23 2020 at 11:45):

Don't mention it.

#### Jasmin Blanchette (Apr 23 2020 at 11:45):

There were over a dozen hammer systems over time, in various systems.

#### Jasmin Blanchette (Apr 23 2020 at 11:46):

But Sledgehammer was the first that was actually useful and usable, starting around the end of 2008.

#### Jasmin Blanchette (Apr 23 2020 at 11:47):

Sledgehammer's secret was its architecture: relevance filter (most don't have that) + efficient translation (that leaves first-order stuff alone) + reconstruction using an all-purpose ATP built directly into Isabelle (metis).

#### Jasmin Blanchette (Apr 23 2020 at 11:48):

Most other systems I can think of, including recent work such as SMTCoq (AFAIK), don't do relevance filtering. Users have to come up with an exaustive list of potentially relevant lemmas themselves. That in practice makes the tool 100 times less useful.

#### Jasmin Blanchette (Apr 23 2020 at 11:48):

It's a bit like using super directly.

#### Jasmin Blanchette (Apr 23 2020 at 11:49):

For reconstruction, metis is like super, roughly, but substantially faster. Maybe Lean 4 will fix that finally.

#### Jasmin Blanchette (Apr 23 2020 at 11:52):

Concerning "hot topic": I hear left and right about people working on hammers, e.g. based on Dedukti and what not. I think Assia is supervising a student about this. And there are, like, 3 ERC grants at the same time about hammers to some extent (Cezary's, Josef's, and mine -- the goal with Matryoshka is to have HO ATPs we can integrate in proof assistants). But it's still a small fraction of papers at, say, CPP/ITP, so I'd go with "active area of study".

#### Kevin Buzzard (Apr 23 2020 at 11:53):

I found it hard to google for information about hammers, apparently there is some popular tool with a metal head which the word is also used for. I tried "Isabelle Hammer" but to my surprise just managed to find a big list of people on Linkedin called Isabelle Hammer.

#### Jasmin Blanchette (Apr 23 2020 at 11:53):

Finally, for AI in hammers, you have to look at HOLyHammer and what Cezary Kaliszyk and Josef Urban have been doing for, like, 8 years now at least in Cezary's case and 20 for Josef.

#### Jasmin Blanchette (Apr 23 2020 at 11:54):

Well start with "Hammering towards QED". We even made the title Briton-friendly. (Don't worry; the rest of the paper is in proper, American English.)

#### Jasmin Blanchette (Apr 23 2020 at 11:55):

There's also a paper called "More SPASS with Isabelle". Given that SPASS means "fun" in German, make sure to Google for it with parental control on.

#### Jasmin Blanchette (Apr 23 2020 at 11:56):

Not so surprised. My real estate agent was called Bibi Hammer.

#### Kevin Buzzard (Apr 23 2020 at 11:57):

I think I have more than enough now; thanks.

#### Reid Barton (Apr 23 2020 at 12:01):

Jasmin Blanchette said:

Its four authors can be considered the main hammer people (Sledgehammer, $\mathrm{Miz}\mathbb{AR}$, HOLyHammer, CoqHammer).

Sounds like some theorem provers/Avengers crossover

#### Jasmin Blanchette (Apr 23 2020 at 12:12):

The four riders of the acoqalypse.

Last updated: May 17 2021 at 22:15 UTC