proof shortening

Stream: Is there code for X?

[Jared green]

if i already have a tactic mode proof of something, is it possible, just knowing its length and what theorems and tactics it calls, to use aesop or something similar to get a shorter one? how would one do it? no example, just wondering if its possible.

[Yury G. Kudryashov]

AFAIK, the only available options are (1) look at the proof and try to do it yourself, and (2) post it on Zulip and wait till someone golfs it for you.