Welcome!

Stream: Machine Learning for Theorem Proving

[Jason Rute]

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]

@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]

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]

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

[Jason Rute]

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

[Mario Carneiro]

Why can't they be the same stream?

[Mario Carneiro]

(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]

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]

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

[Jason Rute]

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