Tool for cleaning / compressing proofs?

Stream: Machine Learning for Theorem Proving

[Bartosz Piotrowski]

Does anyone know of a tool for programmatically cleaning, compressing, or otherwise optimizing proofs in Lean? This would be useful in the context of proving with LLMs, which are know to introduce redundant steps. I'm aware of the ImProver work that uses LLMs to rewrite proofs, in particular, to shorten them. But I thought that maybe we have some purely symbolic tool for that available.

[Jared green]

unfortunately there is not a symbolic tool for proof shortening available.

[Bolton Bailey]

Here are two tools somewhat along these lines I've been told about before:

• Tactic script optimization for aesop
• ImProver (which you mentioned)

I would also be interested in anyone who knows things I can add to this list.

[Bartosz Piotrowski]

Thanks a lot! I'll definitely check Tactic Script Optimisation, sounds relevant.

[Jannis Limperg]

I'm currently working on this. Hopefully I'll be allowed to open-source it.

I thought the Aesop stuff would generalise nicely, but now that I'm actually working on the more general problem, I'm finding that it's quite specific to Aesop's needs.

[Bartosz Piotrowski]

Thank you Jannis, a general proof optimizing / cleaning tool would be definitely useful. Tell me, please, in case you are able to share something!