Jason Rute (Aug 09 2020 at 13:50): Jason Rute (Aug 09 2020 at 13:50):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.
Jason Rute (Aug 09 2020 at 13:51):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.
Jason Rute (Aug 09 2020 at 13:51):Also, it is a go-to place for questions about HOList it seems. The N2Formal folks will respond if pinged.
Jason Rute (Aug 09 2020 at 13:53):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.
Jason Rute (Aug 09 2020 at 13:55):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: Sep 09 2024 at 05:02 UTC