Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Welcome!

Jason Rute (Jan 14 2020 at 00:19):

I've created this stream as a place to discuss AI and machine learning for theorem proving. I put it in the Lean Zulip because this is a great and vibrant community, and I think there is a strong desire to try out machine learning in Lean. However, my hope is that this can be a common place to talk about AI & ML for TP beyond Lean as well. For example, a number of us have been having deep conversations about HOList. We've mapped out its gRPC API and have been discussing many of it's design decisions. We'd love to open up this and other conversations to a wider audience.

Jason Rute (Jan 14 2020 at 01:03):

@Josef Urban @Bartosz Piotrowski @Christian Szegedy @Sarah Loos @Stanislas Polu @Jesse Michael Han @Brando Miranda You all (among others) might be interested in this stream.

Christian Szegedy (Jan 14 2020 at 01:10):

Thanks Jason, I really loved your HOList walkthrough Jupyter notebook. Also, in the long term, I am very excited about the direction of integrating HOList with Lean as well.

Simon Cruanes (Jan 14 2020 at 01:11):

I'm curious, why is there a ML for theorem proving stream but not an ATP for theorem proving one? :p

Jason Rute (Jan 14 2020 at 01:12):

Feel free to start one. :) I'd subscribe.

Mario Carneiro (Jan 14 2020 at 01:14):

Why can't they be the same stream?

Mario Carneiro (Jan 14 2020 at 01:15):

(I'm asking as an outsider. Perhaps they look different in implementation but to an ITP user one automation is as good as another)

Simon Cruanes (Jan 14 2020 at 01:20):

Why can't they be the same stream?

Well I'd see ML as a (small? :crazy:) subset of the techniques of ATP for ITP, so I agree…

Moses Schönfinkel (Jan 14 2020 at 01:20):

Adam Chlipala would just wrap it all into a single tactic call :).

Jason Rute (Jan 14 2020 at 01:21):

I'm fine with either. I like inclusiveness and open discussion.

Last updated: Dec 20 2023 at 11:08 UTC