posted in Technology

beep@beep@piefed.world

Mathematicians are grappling with the possibility that AI might eclipse them

cross-posted from: https://piefed.world/c/tech/p/1309816/mathematicians-are-grappling-with-the-possibility-that-ai-might-eclipse-them

www.understandingai.org/p/mathematicians-are-grappling-with
www.understandingai.orgMathematicians are grappling with the possibility that AI might eclipse themI talked to 20 mathematicians about rapid AI progress in their field.
CubitOom@CubitOom@infosec.pub

Replying to @⁨beep@piefed.world⁩

LLM mathematical proof exploits theorem proover bugs [to get false statement to be “proven” true]

infosec.exchange/@0xabad1dea/117002106099986943

Infosec Exchangeabadidea (@0xabad1dea@infosec.exchange)Okay, we have a new contender for Most AI Thing to Ever Happen 1) July 25th: someone messes around with an LLM and posts a proof of the Collatz conjecture that does, in fact, verify in the theorem prover. (The AI use is not disclosed on the github page) https://github.com/xrchz/CollatzLean 2) July 26th: several serious bugs are posted in the theorem provers, that in principle could allow a false statement to be "proven" true. They're serious, yes, but no need for panic, because you're not going to blunder into accidentally exploiting the bugs while writing a proof, probably. https://github.com/leanprover/lean-kernel-arena/pull/81 3) July 28th: someone who was right to be very skeptical of the Collatz proof, and had the expertise to study it with a fine-toothed comb, discovered it was exploiting a bug https://github.com/leanprover/lean4/issues/14576 4) The "proof" turns out to be exploiting multiple similar but distinct bugs to pass different solver variants! ⚠️⚠️[IMPORTANT EDIT
en