I just discovered this Zulip (and this stream), thanks to @Théo Zimmermann. I just want to advertise that the Lean Zulip channel also has a similar channel. #Machine Learning for Theorem Proving. If any of you are on the Lean Zulip, I encourage you to check it out. If you are not on the Lean Zulip, you can also find it archived here.
There isn't much Lean specific on the channel, since Lean doesn't yet have any machine learning projects (although I dabble with it, and others have expressed interest). Nonetheless, I do try to keep the stream informed on current research in machine learning and theorem proving, although the research is now moving a bit too fast for me to keep up.
Also, it is a go-to place for questions about HOList it seems. The N2Formal folks will respond if pinged.
I've discussed most of the AI projects for Coq, but it's always possible that I've got details wrong (@Lasse has pointed out a few already) or my opinions miss the point.
Anyway, I think it is great that there are multiple places on the internet to discuss this sort of stuff. I'll regularly check back on this stream (and don't hesitate to @ me), and I encourage you all to check out the Lean stream as well.
Last updated: Feb 06 2023 at 06:29 UTC