[don_esteban]

You can select for 'short proof', or 'elementary proof', or assign the 'cost' of the proof as a some combination of its length, the number and complexity of the new terms it needs to define, and so on.

This might not help you with finding the proof, but once you have a machine that can produce several different proofs, you can select among them and incrementally polish the best one.

I think this is the 'easier' part.

[ainch]

I'm sure you could select for shorter proofs, but then that might be confounding in its own way. I think it's a general problem for LLMs that taste is both subjective and hard to pin down to a single metric. There's a reason mathematicians talk about elegance rather than brevity. Sometimes a long geometric proof with a simple algebraic alternative is still elegant, or elucidates the problem in a new way.

[don_esteban]

Well, there are not that many proofs from 'The Book'.

We are a bit ahead of time, currently I would settle for 'as easy to understand as possible' proof. Not a long, complicated, inpenetrable, mess, that Lean says is correct, but reading it provides no insight.