Zulip Chat Archive

Stream: general

Topic: Starting a Machine Learning for Theorem Proving stream


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):

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


Last updated: Dec 20 2023 at 11:08 UTC