2026-10-07 23:16 UTC
If it’s actually exploiting a bug in a formal system, no. If it’s a natural-language (unformalized) document which no one can understand, no. On the other hand a formal proof not using bugs which can’t be understood, is still considered a proof, though its value is lower than an understandable proof. The prototypical example before LLMs was the proof of the four-color theorem which relied on computer-checked casework.
Replies (1)
-
@Amoeba_Girl@awful.systems 2026-10-09 08:59
I suppose what it comes down to is, if OpenAI couldn’t be bothered to try and elucidate their results, or even try to separate nonsensical exploits from genuine proofs, I don’t understand why mathematicians shouldn’t treat all of it as worthless instead of doing unpaid PR work for them.