Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Welcome!


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jason Rute (Jan 14 2020 at 01:12):

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

view this post on Zulip Mario Carneiro (Jan 14 2020 at 01:14):

Why can't they be the same stream?

view this post on Zulip 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)

view this post on Zulip 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…

view this post on Zulip Moses Schönfinkel (Jan 14 2020 at 01:20):

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

view this post on Zulip Jason Rute (Jan 14 2020 at 01:21):

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


Last updated: May 09 2021 at 23:10 UTC