[evenhash]

The proof is not written in Lean, though. It’s written in English and requires validation by human experts to confirm that it’s not gibberish.

[vatsachak]

Yeah, but I wouldn't be surprised if they train the model on verification assisted by Lean