Crank author at a crank “institution” - I can’t assess whether the OpenAI paper is accurate but I highly doubt this is going to be the paper to disprove it.
Genuine question - this is so hard for me to follow. Not that I could follow the original disproof anyways. But how is "truth" determined when the effort required to validate is so high?
That's different though. Understanding the spec of Fermat's last theorem is simple. Here, you already need to know some mathematics just to understand the spec.
These AI generated proofs have something akin to the quantum algorithms that can generate a response that would take 1 billion years of processing to finish on a classical computer. How do you test them to see if the result was correct?
Maybe there's an error, but much of this write-up reads like nonsense to me. The assertion that a semidirect product with an abelian factor must admit that factor in its center is absolutely false. This is actually acknowledged later in this article, but is handwaved away in incomprehensible fashion.
> The gap has two independent consequences, each sufficient to invalidate the claimed disproof. The first is structural.
Then the classic coding agents negation of earlier evidence, instaed of just updating to use new references, they mention that they changed old to new:
> The publicly released monolithic file ConnesRigidity.lean (37,000+ lines) does not use the names CocycleExtension, ZeroCocycle, or TwistedCocycle that appeared in the earlier modular source files (CocycleExtension.lean, ICC.lean, CrossedClosure.lean). However, the identical mathematical construction is present under different names. The following table gives the correspondence, with line numbers in the published file.
> This is the same zero-cocycle / twisted-cocycle structure identified in the earlier modular
source files, confirming that the structural analysis of this note applies to the published code
And some other Claud-y stuff:
> Why both paths are closed. A successful defence would have to close both paths simultaneously
> This case illustrates a failure mode that is becoming increasingly well documented in the literature on AI-assisted formal mathematics: the gap between what a formal proof verifies and what it means. The Lean kernel certifies that a proof term inhabits a given type; it does not certify that the type faithfully encodes the intended mathematical claim. As Tao has emphasised
And afterwards I cross-verified with Pangram 4 which I trust, it marked the preamble/starting stuff as 100% AI-generated.
The author of this paper has also apparently published a proof of the Riemann Hypothesis. yeah idk if they should be trusted as an authority on this.
Crank author at a crank “institution” - I can’t assess whether the OpenAI paper is accurate but I highly doubt this is going to be the paper to disprove it.
link for the curious https://philarchive.org/archive/NIEPOT-5
Author is a crackpot. She does not meaningfully engage with anyone who points out the key flaw in her counterargument. See the thread here https://x.com/AcerFur/status/2083649346294382803
Genuine question - this is so hard for me to follow. Not that I could follow the original disproof anyways. But how is "truth" determined when the effort required to validate is so high?
It's a common problem in math. The famous proof for Fermat's last theorem took 2 years to validate.
That's different though. Understanding the spec of Fermat's last theorem is simple. Here, you already need to know some mathematics just to understand the spec.
These AI generated proofs have something akin to the quantum algorithms that can generate a response that would take 1 billion years of processing to finish on a classical computer. How do you test them to see if the result was correct?
Maybe there's an error, but much of this write-up reads like nonsense to me. The assertion that a semidirect product with an abelian factor must admit that factor in its center is absolutely false. This is actually acknowledged later in this article, but is handwaved away in incomprehensible fashion.
This "paper" itself is 100% AI-generated...
What makes you say that? Not dunking, I skimmed it (I’m in no way at this level) and didn’t see anything outright Claud-y.
This immediately struck me as Claud-y:
> The gap has two independent consequences, each sufficient to invalidate the claimed disproof. The first is structural.
Then the classic coding agents negation of earlier evidence, instaed of just updating to use new references, they mention that they changed old to new:
> The publicly released monolithic file ConnesRigidity.lean (37,000+ lines) does not use the names CocycleExtension, ZeroCocycle, or TwistedCocycle that appeared in the earlier modular source files (CocycleExtension.lean, ICC.lean, CrossedClosure.lean). However, the identical mathematical construction is present under different names. The following table gives the correspondence, with line numbers in the published file.
> This is the same zero-cocycle / twisted-cocycle structure identified in the earlier modular source files, confirming that the structural analysis of this note applies to the published code
And some other Claud-y stuff:
> Why both paths are closed. A successful defence would have to close both paths simultaneously
> This case illustrates a failure mode that is becoming increasingly well documented in the literature on AI-assisted formal mathematics: the gap between what a formal proof verifies and what it means. The Lean kernel certifies that a proof term inhabits a given type; it does not certify that the type faithfully encodes the intended mathematical claim. As Tao has emphasised
And afterwards I cross-verified with Pangram 4 which I trust, it marked the preamble/starting stuff as 100% AI-generated.
One of mathematicians working at OpenAI refuted those claims directly on X - https://x.com/AcerFur/status/2083656978719719601
Opus 5 says the disproof is wrong.
does this show Lean is not bulletproof?