curmudgeoning

Stream: Machine Learning for Theorem Proving

[Daniel Selsam]

Speaking as the resident curmudgeon, I'll mention that for what it is worth, I prefer not using "AI" to (presumably) mean "ML".

[Jason Rute]

Does it help that I use both AI and ML in the stream name, or would you prefer it is just ML for TP?

[Daniel Selsam]

Could you please clarify what of relevance is in $AI \setminus (TP \cup ML)$?

[Mario Carneiro]

There is a lot of value in GOFAI for TP that is not specifically ML. ATP stuff comes to mind

[Daniel Selsam]

I assumed that was already part of the "TP" part.

[Mario Carneiro]

Oh... I guess if you intend to subtract everything in TP then there isn't much of relevance to this chat. Maybe a chess AI?

[Simon Hudon]

I guess when subtracting TP, you need to only subtract the AI stuff that has already been successfully used in TP, not all that could potentially be relevant

[Daniel Selsam]

I fear that continuing this witty repartee may be problematic, since it is hard to read between the lines on text-only chat. I also realize that we may all have different perspectives on the infamously shape-shifting phrase "AI", and that its scope and proper use is a big discussion/debate in and of itself. I wasn't trying to be annoying, and I'll stay out of it.

[Jason Rute]

If we can change the name, I'd happy to do it now. I didn't realize I was going to start an argument with the name. But I can't find a way to do it (or to fix the typo in the stream description).

[Simon Hudon]

I think the only way is to create a new stream and encourage everyone to unsubscribe from this one. Luckily, there doesn't seem to be contents yet

[Simon Hudon]

However, you do take the risk of some people not unsubscribing and using it instead of the other one

[Daniel Selsam]

Sebastian Ullrich has stream-name-changing authority.

[Daniel Selsam]

But he is in Europe and probably asleep already.

[Jason Rute]

Does he have stream archiving powers? If so, I can make a new one, and he can archive/delete this when awake.

[Daniel Selsam]

I don't know if he can archive but he can very likely delete.

[Jason Rute]

Ok. I'm making a new one.

[Jason Rute]

Use this instead. https://leanprover.zulipchat.com/#narrow/stream/219942-Machine-Learning.20for.20Theorem.20Proving

[Mario Carneiro]

I have stream name editing powers here, but I'm not sure why there is a need to be exclusionary here

[Mario Carneiro]

I can also delete streams but first figure out what you want to do with all this

[Jason Rute]

If you can edit stream names, then maybe delete the new one I just made, change the name of this one to that one, and we can be happy? The welcome messages are basically the same for both.

[Mario Carneiro]

What's wrong with just AI for TP? If the only interesting AI systems are in ML then so be it but I don't see any reason to declare that at the outset

[Jason Rute]

Thanks @Mario Carneiro!

[Brando Miranda]

Hi everyone! Just saw this conversation. I'm curious, did we create new streams for this? I don't want to miss any on the great topic using any tools for TP.

[Jason Rute]

This was during the very first hours of this stream. It was all worked out then. You should be fine.