alt Hacker NewsI have the same questions about human mathematicians!
I can't tell if xkcd #435 is still true, or if math is just as mushy as everything else seems to be. When a math proof can only be understood by a handful of people, what does that mean about that proof? I think the LLMs are pushing a problem that existed already and pushing it further.
That's why OpenAI also published machine-checkable proofs.
The process is very, very faintly similar to running a typechecker over your software sources.