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