2 ms·
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 subj
by ainch 2mo ago
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 2mo agoWell, 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.