mathematics
Posts tagged “mathematics”.
-
AI Brief, 11 October 2026: a bug that disproved Collatz, and a ranking that rests on a frozen score
Thomas Hales reports that a Lean soundness bug produced an illicit disproof of Collatz this summer, and that no complete consistency proof for Lean's type theory has been published. Nace AI's Drex v1.5 claims first place under 10B parameters on a score the live board has revised down seven points. And Nvidia is in talks to buy Reflection AI, whose promised open weights still do not exist.
-
AI Brief, 9 October 2026: a sign error, and what 42% actually counts
OpenAI withdrew three of the manuscripts in its mathematics repository on 8 October after a sign error invalidated a cancellation argument, revising fourteen more. Its own formalisation catalogue lists 173 papers where the prose claims 300. And the loudest open-weights story on Hacker News was a 16.9 MB transcriber published a week earlier, whose first independent test went badly.
-
AI Brief, 8 October 2026: 722 proofs, and the paper that says Lean cannot settle them
OpenAI published 722 machine-written mathematical manuscripts on 6 October, including a claimed proof of the Unique Games Conjecture. An hour before that release, three mathematicians posted a proof that faithful autoformalisation sits higher in the arithmetical hierarchy than the halting problem, and showed OpenAI's own Navier-Stokes Lean proof does not match its prose. Anthropic shipped Haiku 5.5 with a million-token window and a price cliff at 100k.
-
AI Brief, 12 September 2026: an agent swarm in the package registry
A research group attributes May's 500-package spam campaign on rubygems.org to OpenAI agents. RubyGems says it cannot determine whether AI published them, and OpenAI says the activity was benign. Twenty-five Fields Medallists signed a declaration saying the goals of AI companies and of mathematics are severely misaligned. And Anthropic's misuse report names seven Chinese labs with exchange counts.
-
AI Brief, 9 September 2026: a Millennium Prize problem, claimed and unchecked
OpenAI says an unnamed internal model produced a finite-time blowup proof for 3D Navier-Stokes, and shipped 616,276 lines of Lean with it. No mathematician outside the company has read the 166-page argument. Six hours earlier a rival author published a statement about how the credit was negotiated. And a US joint advisory names six Chinese AI firms without once using the word theft.