automatic golfing?

Stream: general

[Ralf Stephan]

Have there been attempts at the task "Take a (working) Lean4 proof and simplify it by 1. using 'better suited' lemmas; or 2. removing redundancies in structure"? To be able to apply machine learning, there would be need for training data. Isn't it bad if, while formalizing, we discard the first attempt(s) that work, instead of somehow documenting them?

[Johan Commelin]

I think it would be cool to have a plugin that records such things. Continue.dev has stuff in that direction.

[Johan Commelin]

As a first approximation, find all commits with golf in the msg and train on their diffs

[Ralf Stephan]

Maybe establish some tag for such commits. But golfs within PRs get lost from squashing.

[Bolton Bailey]

I have #9320 to golf simp calls, but some people pointed out that while this would make proofs shorter it might also make proof states more complicated, so it got forgotten.