ProofOptimizer

Stream: Machine Learning for Theorem Proving

[Junyan Xu]

FYI
Finally we have a golfing model, looks exciting to me. It seems they are focused on golfing LLM-generated proofs and didn't attempt to golf mathlib proofs though.
https://x.com/minimario1729/status/1980262731099037915
https://proof-optimizer.github.io/

[Kim Morrison]

It's a bit scary that their collection of input proofs which the attempt to golf during training seems to be entirely generated by GoedelProver. Surely a more diverse set of proofs would be better?

[Bolton Bailey]

This is great, I think this branch of work is pretty important. Some questions:

Is (there any plan to make) the model or code available open source?
What happens if the model is run on human-written proofs from mathlib? Could this reduce compile time and file length while keeping human-readability intact?

[Justin Asher]

This is a well-written paper! Congrats to the authors.

We ideally should just have a repository of RL environments that we train a single large coding model on to do all of these tasks. I do not think fine-tuning small models for specific Lean related tasks is ideal, as there should be a decent amount of transfer learning going on between the tasks.