News for hackers. Stuff that matters.

bamb008

Re:Classification of Finite Simple Groups Formalized in Lean on Tuesday October 27, 2026 @01:58PM (#50263183)
In [1] they claim:

>However, there were 34 noteworthy deviations from the published record that needed to be resolved, the most substantial of which related to the Unbalanced Group Theorem.

[1]https://axiommath.ai/research/the-enormous-theorem-formalize...

Doesn't this make it seem like Wang had the wrong intuition, if her meyhod does not generalize? She proved Kakeya only in dimension 3, and also not prove the Hausdorff 3D Kakeya. In retrospect it seems humans were asking the wrong question, if a couple dozen pages long manuscript can subsume so many other efforts.

AI has only been able to advance the math frontier for a couple of months, fully grasping the applications, connections, and possible generalizations takes longer.

The idea that OpenAI's proofs are fake is contradicted by the response of mathematicians. Were they fake, mathematicians would not consider this release important enough to comment upon[1,2], as vixra always provided a steady supply of such writings. Nor would they be able to write expositions and simplifications, of which several are published each day on arxiv (just search OpenAI on arxiv to find them).

But perhaps mathematicians are no longer able to be the best judge if a proof is valid. Yet nobody but them is able to even understand what is claimed to have been resolved.

It is really strange to see mathematicians of the highest rank taking these results seriously[3], holding lectures explaining them, yet see it dismissed here as a mass psychosis. [1]https://smf.emath.fr/actualites-smf/20-10-26-communique-sur-... [2]https://www.mathsoc.jp/publicity/news20261016.html [3]https://terrytao.wordpress.com/2026/10/19/a-sketch-of-the-pr...

>Every major statement I've seen come out of the math community on this matter reads as well thought-through, humble, reasoned, and deeply human.

Can't disagree with "deeply human", but I wouldn't always use it in a positive sense:

https://proofsandprompts.com/2026/09/10/open-letter-about-th...

>Participation in an event so closely associated with Anthropic and OpenAI could plausibly negatively impact the future reputations of participants

Re:OpenAI might have stolen another major proof on Thursday September 10, 2026 @05:23AM (#49640833)
When Thom, the mathematician who now alleges plagiarism, posted his digestion [1] of OpenAI's construction of a non-sofic group, he does not mention the proof being familiar. He even calls the crucial argument clever, without noting he thought of it first. [1]https://mathoverflow.net/a/513885
Re:Formalization of the Solution to the Hopf Problem on Monday August 31, 2026 @06:47AM (#49508130)
An exposition of the Alpöge-Claude construction, by a mathematician working in this area: https://philip-engel.github.io/S6.pdf