Email Gateway (May 29 2025 at 14:13): Email Gateway (May 29 2025 at 14:13):From: Lawrence Paulson <lp15@cam.ac.uk>
These days one frequently comes across a phrase like "a hammer is a link between an ITP and ATPs", followed by numerous references to papers on these systems. Does anybody have numerical data on how heavily these various hammers are used?
Larry
Email Gateway (Jun 04 2025 at 07:48):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
I'm not aware of any numerical data on the use of the other hammers. I have only anecdotal bits of information to offer, e.g., that HOL(y)Hammer was useful to complete the Flyspeck project.
Jasmin
--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html
On 29. May 2025, at 16:13, Lawrence Paulson <lp15@cam.ac.uk> wrote:
These days one frequently comes across a phrase like "a hammer is a link between an ITP and ATPs", followed by numerous references to papers on these systems. Does anybody have numerical data on how heavily these various hammers are used?
Larry
Email Gateway (Jun 04 2025 at 09:26):From: Fabian Huch <huch@in.tum.de>
Jiang et al. claim that sledgehammer-generated proofs make up 2.40% of
proof steps in their training set that includes LISA (which is based on
the AFP from 2021 AFAIK) [1].
I am not sure how accurate that is though: The paper claims that "metis,
meson, smt are exclusive to sledgehammer" which is not quite correct,
and seemingly the numbers are based on that.
Fabian
[1] Jiang, Albert Qiaochu, et al. "Thor: Wielding hammers to integrate
language models and automated theorem provers." /Advances in Neural
Information Processing Systems/ 35 (2022): 8360-8373.
On 6/4/25 09:48, Jasmin Blanchette wrote:
I'm not aware of any numerical data on the use of the other hammers. I
have only anecdotal bits of information to offer, e.g., that
HOL(y)Hammer was useful to complete the Flyspeck project.Jasmin
--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.htmlOn 29. May 2025, at 16:13, Lawrence Paulson <lp15@cam.ac.uk> wrote:
These days one frequently comes across a phrase like "a hammer is a
link between an ITP and ATPs", followed by numerous references to
papers on these systems. Does anybody have numerical data on how
heavily these various hammers are used?Larry
Email Gateway (Jun 04 2025 at 09:36):From: Lawrence Paulson <lp15@cam.ac.uk>
I frequently hand-edit the output of sledgehammer (and I encourage others to do the same, as it can be messy), but does anybody out there invoke these methods directly?
It is certainly true that in HOL Light, a call to MESON_TAC would definitely have been created by hand.
Larry
On 4 Jun 2025 at 10:26 +0100, Fabian Huch <huch@in.tum.de>, wrote:
I am not sure how accurate that is though: The paper claims that "metis, meson, smt are exclusive to sledgehammer" which is not quite correct, and seemingly the numbers are based on that.
Email Gateway (Jun 04 2025 at 09:43):From: Jan van Brügge <jan@vanbruegge.de>
Not with arguments, but sometimes try0 returns a "by metis" or "by meson", so those do not come from sledgehammer.
04.06.2025 11:36:43 Lawrence Paulson <lp15@cam.ac.uk>:
I frequently hand-edit the output of sledgehammer (and I encourage others to do the same, as it can be messy), but does anybody out there invoke these methods directly?
It is certainly true that in HOL Light, a call to MESON_TAC would definitely have been created by hand.
Larry
On 4 Jun 2025 at 10:26 +0100, Fabian Huch <huch@in.tum.de>, wrote:I am not sure how accurate that is though: The paper claims that "metis, meson, smt are exclusive to sledgehammer" which is not quite correct, and seemingly the numbers are based on that.
Email Gateway (Jun 04 2025 at 10:34):From: Manuel Eberl <manuel@pruvisto.org>
I very occasionally use them in situations where I would normally use
"blast" (i.e. basic logic/set theory and nothing else) but "blast" fails
for some reason. Usually it is then also try0 that directs me towards them.
However, one very specific case where I sometimes use metis even without
being told to by try0 is if I already know that for every x there exists
a y such that "P x y" holds and now I want to obtain a function f such
that "P x (f x)" holds for any x. Metis is very good at applying the
axiom of choice in such situations (presumably because it skolemises
everything anyway?).
Cheers,
Manuel
On 04/06/2025 11:38, Jan van Brügge wrote:
Not with arguments, but sometimes try0 returns a "by metis" or "by
meson", so those do not come from sledgehammer.04.06.2025 11:36:43 Lawrence Paulson <lp15@cam.ac.uk>:
I frequently hand-edit the output of sledgehammer (and I encourage
others to do the same, as it can be messy), but does anybody out
there invoke these methods directly?It is certainly true that in HOL Light, a call to MESON_TAC would
definitely have been created by hand.Larry
On 4 Jun 2025 at 10:26 +0100, Fabian Huch <huch@in.tum.de>, wrote:I am not sure how accurate that is though: The paper claims that
"metis, meson, smt are exclusive to sledgehammer" which is not
quite correct, and seemingly the numbers are based on that.
Email Gateway (Jun 04 2025 at 10:51):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes, this! Rather than making an ugly definition using the SOME / @ descriptor, just “obtain" the function you want. Here metis needs no arguments but often sledgehammer fails to find it.
Larry
On 4 Jun 2025, at 10:58, Manuel Eberl <manuel@pruvisto.org> wrote:
However, one very specific case where I sometimes use metis even without being told to by try0 is if I already know that for every x there exists a y such that "P x y" holds and now I want to obtain a function f such that "P x (f x)" holds for any x. Metis is very good at applying the axiom of choice in such situations (presumably because it skolemises everything anyway?).
Email Gateway (Jun 04 2025 at 17:26):From: Tjark Weber <tjark.weber@it.uu.se>
On Wed, 2025-06-04 at 09:36 +0000, Lawrence Paulson wrote:
I frequently hand-edit the output of sledgehammer (and I encourage others to do the same, as it can be messy), but does anybody out there invoke these methods directly?
When I know which lemmas are needed to prove a goal, I very occasionally write "by (metis foo bar baz)" if alternatives such as "by (auto simp add: foo bar baz)" don't work. (Sometimes sledgehammer can also find these lemmas, sometimes it can't.)
Regarding your original question, Geoff Sutcliffe might have some usage data for the TPTP web interface. (Of course, this would not cover locally installed solvers.)
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Jun 04 2025 at 18:05):From: Lawrence Paulson <lp15@cam.ac.uk>
Back in 2015, Geoff mailed me and mentioned that Isabelle users via sledgehammer
“are the main users of the SystemOnTPTP service, by a loooong way.”
These days, it may be different. People mainly run provers locally.
This was in the context of a broader discussion suggesting that sledgehammer (and possibly similar hammers) are the main application of automated theorem proving.
Larry
On 4 Jun 2025, at 18:19, Tjark Weber <tjark.weber@it.uu.se> wrote:
Regarding your original question, Geoff Sutcliffe might have some usage data for the TPTP web interface. (Of course, this would not cover locally installed solvers.)
Email Gateway (Jun 04 2025 at 18:51):From: Makarius <makarius@sketis.net>
On 04/06/2025 20:05, Lawrence Paulson wrote:
Back in 2015, Geoff mailed me and mentioned that Isabelle users via sledgehammer
“are the main users of the SystemOnTPTP service, by a loooong way.”
These days, it may be different. People mainly run provers locally.
Initially the suite of local ATPs was somewhat incomplete, but we have moved
to local provers as default some years ago.
This usually works better than the remote "software-as-a-service" approach,
but failure can still happen --- due to odd OS side-conditions (on all platforms).
Makarius
Email Gateway (Jun 05 2025 at 09:59):From: Filip Smola <cl-isabelle-users@lists.cam.ac.uk>
Metis is often one of the methods I try if I think I have all the needed facts
on hand. When it works, it is often the fastest one from the ones I try. And
there are sometimes cases where Sledgehammer doesn't find a proof (at least
with the default timeout) but I manage to put one together by hand, often
needing metis.
Filip
\-------- Original Message --------
On 04/06/2025 10:36, Lawrence Paulson wrote:
I frequently hand-edit the output of sledgehammer (and I encourage others to
do the same, as it can be messy), but does anybody out there invoke these
methods directly?It is certainly true that in HOL Light, a call to MESON_TAC would
definitely have been created by hand.Larry
On 4 Jun 2025 at 10:26 +0100, Fabian Huch <huch@in.tum.de>, wrote:
>
>
I am not sure how accurate that is though: The paper claims that "metis,
meson, smt are exclusive to sledgehammer" which is not quite correct, and
seemingly the numbers are based on that.
Last updated: Jun 20 2025 at 16:26 UTC