Zulip Chat Archive

Stream: new members

Topic: Does Lean list choices?


Daniel Donnelly (Aug 25 2019 at 15:16):

Hi. Was wondering what kind of conclusions Lean can come to on its own, and thus if it can "list choices" when you're proving something. For instance if it knows f : A -> B is a function and I assert that there's an x in A, then can I "list choices" here one of which would be "there exists an element f(x) in B". I'm still learning Lean, so not sure how it all works. I can work with it either way for my app. For instance the suggested choices pane in the app could be constructed by user statistics or simply ordering the choices by "how many times did this choice appear in the steps of a successful proof". That should be easy enough and not require much on the server side to aggregate the usage stats and update each user's copy.

Johan Commelin (Aug 25 2019 at 15:20):

I think that what you would want is some sort of diagram chasing tactic. At the moment there is no such thing. But we are approaching additive/abelian categories in mathlib. Once we have those, such a tactic will be on several peoples wishlist.

Daniel Donnelly (Aug 25 2019 at 15:20):

So you have it for other things than diagram chasing?

Johan Commelin (Aug 25 2019 at 15:21):

There is tidy.

Johan Commelin (Aug 25 2019 at 15:21):

For a nice story of what it does (more or less), you should read the paper by Gowers and Ganesalingam.

Johan Commelin (Aug 25 2019 at 15:21):

I'm quite sure that you'll find it interesting.

Johan Commelin (Aug 25 2019 at 15:22):

https://arxiv.org/abs/1309.4501

Daniel Donnelly (Aug 25 2019 at 15:23):

Thanks! I will look at it


Last updated: Dec 20 2023 at 11:08 UTC