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.)