Starting a Machine Learning for Theorem Proving stream

Stream: general

[Jason Rute]

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]

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

[Reid Barton]

This sounds entirely sensible to me

[Patrick Massot]

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]

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