Zulip Chat Archive

Stream: general

Topic: Starting a Machine Learning for Theorem Proving stream


view this post on Zulip Jason Rute (Jan 12 2020 at 16:22):

For the last few months a number of us have been having private conversations about Machine Learning for theorem proving, specifically taking about HOList and speculating about integrating Lean 3. I'd like to make this discussion public. It isn't 100% a Lean topic, but this is a great community and where most of the conversations have been happening. How does the community feel if we start a Steam for Machine Learning for Theorem Proving (and if we spend a lot of time talking about HOList and similar systems)?

view this post on Zulip Jason Rute (Jan 12 2020 at 16:27):

cc @Markus Rabe @Brando Miranda @Jesse Michael Han @Stanislas Polu

view this post on Zulip Reid Barton (Jan 12 2020 at 17:04):

This sounds entirely sensible to me

view this post on Zulip Patrick Massot (Jan 12 2020 at 17:46):

I think there is no problem creating more streams. Nobody is forced to subscribe, and I don't think we are close to exhausting Zulip resources. In addition I'm convinced this is a good topic, but this opinion is irrelevant.

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

I made the stream here: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving


Last updated: May 16 2021 at 05:21 UTC