Diffgeometer1 on Nostr: if one knows a result is true but the proof is long and ugly the challenge is to ...

if one knows a result is true but the proof is long and ugly the challenge is to develop new tools that will replace the long and ugly proof with one that is elegant. It’s in this area where humans can excel over LLMs I would think.