You know how AI proofs are supposed to be credible because of formalization with Lean? There is another problem… apparently Lean4 hasn’t actually been fully formally verified. And in fact could have more bugs lurking in it, maybe even some foundational problems… Lesswrong post explaining the problems. OpenAI can more easily market that their AI is intended to fully replace mathematicians, and that this is only the herald of their general superintelligence (and not that math is the only thing working out for them). Yeah, this has been driving me crazy… reading places like hackernews or r/singularity, I keep seeing people assuming mathematicians and just bitter or engaging in sour grapes and that is why they are complaining about the “proofs” OpenAI dumped out. Like it is just some small niggling detail that the proofs can’t be read by humans and that Lean may have bugs and that some of OpenAI’s proofs have already been shown to have critical mistakes.