Metis Theorem Prover in Lean

Stream: general

[A. Stone Olguin]

Hi all, I was wondering if anyone knows if anyone has worked on implementing the metis theorem prover in Lean similar to how it was implemented in Isabelle. Any info helps, thanks!

[Gabriel Ebner]

Some time back I wrote a superposition in Lean, which fills a similar niche as metis. https://github.com/leanprover/super
Lean 3 was quite slow though, making this tool less useful than it could be. Lean 4 is out now, so at some point I am going to revisit super and see if I can make it faster this time.

[Max]

On a related note, is there any ongoing projects at a Sledgehammer for Lean4?

[Patrick Massot]

There are a lot of people who are at least thinking really seriously about whether this is the right question to ask.

[Patrick Massot]

see https://matryoshka-project.github.io/ in particular

[Brandon Brown]

Isnt Lean-GPTF basically developing into a sledgehammer?

[Alexander Bentkamp]

Brandon Brown: Isnt Lean-GPTF basically developing into a sledgehammer?

In the sense that both offer general purpose automation, yes, but the technology behind the scenes is very different. GPTF relies on neural networks, whereas sledgehammer calls first-order automated theorem provers, such as Vampire or E.

[Max]

Nice, gonna read through those sources! Thanks :)