# Zulip Chat Archive

## Stream: Machine Learning for Theorem Proving

### Topic: Isabelle and neural theorem proving

#### Jason Rute (May 27 2022 at 14:20):

There are two (well three) papers recently on neural theorem proving for Isabelle which is great. In many ways Isabelle, with its powerful Sledgehammer was at the front of automated theorem proving applied to interactive theorem proving. But now there are works taking this to the next level by integrating neural tools into Isabelle. I have to admit I haven't looked at either of these papers in detail yet, but I want to mention them here:

#### Jason Rute (May 27 2022 at 14:20):

- Isabelle ENIGMA
- Title: The Isabelle ENIGMA
- Authors: @Zar Goertzel, Jan Jakubův, Cezary Kaliszyk, @Miroslav Olšák, Jelle Piepenbrock, @Josef Urban
- arXiv: https://arxiv.org/abs/2205.01981

- Thor:
- Title: Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
- Authors: @Albert Jiang, @Wenda Li, @Szymon Kitowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, @Yuhuai Tony Wu , Mateja Jamnik
- Twitter announcement: https://twitter.com/AlbertQJiang
- arXiv paper: https://arxiv.org/abs/2205.10893

#### Jason Rute (May 27 2022 at 14:21):

My very quick understanding is that the first uses machine learning *inside* Sledgehammer to improve the first order theorem prover and premise selector (lemma selector) used by Sledgehammer. This is similar to the previous ENGIMA projects but focusing on Isabelle and the Archive of Formal Proofs. The second on the other hand uses machine learning *outside* Sledgehammer more similar to GPT-f and other neural tactic-guiding tools to guide tactics and Sledgehammer, but also to delegate to Sledgehammer for certain tasks like premise selection. Superficially it looks like they are orthogonal and can be combined.

#### Jason Rute (May 27 2022 at 14:22):

The third paper is on autoformalization in Isabelle and deserves its own topic.

#### Albert Jiang (May 27 2022 at 14:44):

Jason Rute said:

- Isabelle ENIGMA

- Title: The Isabelle ENIGMA
- Authors: Zar Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, Josef Urban
- arXiv: https://arxiv.org/abs/2205.01981
- Thor:

- Title: Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
- Authors: Albert Jiang, Yuhuai Tony Wu, Szymon Kitowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Tony Wu , Mateja Jamnik
- Twitter announcement: https://twitter.com/AlbertQJiang
- arXiv paper: https://arxiv.org/abs/2205.10893

I think for Thor, you meant @Wenda Li as the second author :)

#### Jason Rute (May 27 2022 at 14:46):

Fixed.

#### Albert Jiang (May 27 2022 at 14:49):

Jason Rute said:

My very quick understanding is that the first uses machine learning

insideSledgehammer to improve the first order theorem prover and premise selector (lemma selector) used by Sledgehammer. This is similar to the previous ENGIMA projects but focusing on Isabelle and the Archive of Formal Proofs. The second on the other hand uses machine learningoutsideSledgehammer more similar to GPT-f and other neural tactic-guiding tools to guide tactics and Sledgehammer, but also to delegate to Sledgehammer for certain tasks like premise selection. Superficially it looks like they are orthogonal and can be combined.

I've read the Isabelle ENIGMA paper and agree with your understanding on both papers. The ENIGMA paper came out just when we were about to wrap up Thor. Otherwise we would have reached out to see if we can combine the two. It remains a future direction to get neural and symbolic components firmly weaved together in great granularity :)

Last updated: Dec 20 2023 at 11:08 UTC