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)?
Jason Rute (Jan 12 2020 at 16:27):
cc @Markus Rabe @Brando Miranda @Jesse Michael Han @Stanislas Polu
Reid Barton (Jan 12 2020 at 17:04):
This sounds entirely sensible to me
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.
Jason Rute (Jan 14 2020 at 01:06):
Last updated: May 16 2021 at 05:21 UTC