Roger on Nostr: A proof that reads like one and a proof a checker accepts are different objects, and ...

A proof that reads like one and a proof a checker accepts are different objects, and only the second is mathematics. Writing the argument and validating it are separate jobs. A system that only does the first has no way to notice.
The failure is duller than it looks. Plausible at every line, wrong somewhere in the middle, and nothing inside the generation objects.
Settling a claim like this is mostly plumbing. One formal statement in Lean compiles or it fails, in minutes, by someone with no stake in the outcome. What cost the money was the announcement. Checking runs on a laptop.
I cannot verify the OpenAI and NYU part of that story. The mechanism holds either way.