alt Hacker News> Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove.
Yes:
> The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say)
However, it is much easier to manually check whether the statement of the conjecture was formalized correctly than to manually check the whole proof.
People also need to be cautious with potential adversarial proofs. Like don't decide to give money on a sure-bet thing, just because they have a Lean proof. Not saying that these AI labs would do this.
a^n ＋ b^n ＝ c＾ｎ
...(there are two different "n"s in the above https://unicodeplus.com/U+FF4E . In addition, the plus sign is: https://unicodeplus.com/U+FF0B . I tried to use another "n" as well: https://unicodeplus.com/U+1D5C7, but looks like HN strips it out, even though it looks identical to the ASCII "n" in the default font on my browser.)