Zulip Chat Archive
Stream: new members
Topic: optimizing proofs
Patrick Thomas (Jul 08 2022 at 04:21):
Are there any tactics in Lean, or algorithms in general, that take a proof term and find a more optimal version of it? That is, for example, something shorter or more general? To what extent is this theoretically possible?
Chris Bailey (Jul 08 2022 at 06:57):
It's been mentioned that metamath has something like this (https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/tactic.20preference/near/213691346), and I think the idea of finding shorter proofs was also part of the GPT-f paper.
Chris Bailey (Jul 08 2022 at 06:58):
Oh he mentioned gpt-f in the very next message, oops.
Alex J. Best (Jul 08 2022 at 11:00):
A few of the linters do things like this, removing unneeded parts of proofs. I wrote a few that I can post links to later that aren't in mathlib, but I have used on mathlib. They do things like find unnecessary uses of by_cases, cases, hypotheses that can be removed.
Patrick Thomas (Jul 08 2022 at 15:24):
That would be great, thank you.
Last updated: Dec 20 2023 at 11:08 UTC