If I recall correctly there was a proposed proof to the abc conjecture by Mochizuki https://en.wikipedia.org/wiki/Abc_conjecture#Claimed_proofs which was rejected due to being rather inpenetrable to humans. Shouldn't this be an ideal target for LLMs?