Zulip Chat Archive

Stream: new members

Topic: Does Lean list choices?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Daniel Donnelly (Aug 25 2019 at 15:20):

So you have it for other things than diagram chasing?

view this post on Zulip Johan Commelin (Aug 25 2019 at 15:21):

There is tidy.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 25 2019 at 15:21):

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

view this post on Zulip Johan Commelin (Aug 25 2019 at 15:22):

https://arxiv.org/abs/1309.4501

view this post on Zulip Daniel Donnelly (Aug 25 2019 at 15:23):

Thanks! I will look at it


Last updated: May 08 2021 at 04:14 UTC