4 ms·

Just two days ago, a preprint by Julia Stadlmann went up on arXiv [0] improving the prime gap from 246 to 240. Now OpenAI announces Astra has shown a gap of 186

by Cu3PO42 1mo ago

Just two days ago, a preprint by Julia Stadlmann went up on arXiv [0] improving the prime gap from 246 to 240. Now OpenAI announces Astra has shown a gap of 186 [1]. That must really blow. [0] https://arxiv.org/abs/2608.31126 https://arxiv.org/abs/2608.31126 [1] https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/short_gaps.pdf https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16...

bananaflag 1mo ago
Where did you get the link to the pdf? Was it announced somewhere?
htrp 1mo ago
https://github.com/openai/PrimeGaps186 https://github.com/openai/PrimeGaps186
- dang 1mo ago
  https://news.ycombinator.com/item?id=49555257 https://news.ycombinator.com/item?id=49555257
- nateb2022 1mo ago
  I'm surprised the OpenAI employee who pushed this didn't take the minute or two to format README.md to use GitHub-supported LaTeX (https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/writing-mathematical-expressions https://docs.github.com/en/get-started/writing-on-github/wor...) edit: my comment was on the submission for https://github.com/openai/PrimeGaps186 https://github.com/openai/PrimeGaps186 but seems to have been moved to the main Astra submission
  - warkdarrior 1mo ago
    > OpenAI employee Why would you think it was an employee who did the push, instead of a random GPT agent?
well_ackshually 1mo ago
Such a result should be considered worthless: the proof is 10MB of Lean. (https://github.com/openai/PrimeGaps186 https://github.com/openai/PrimeGaps186). I can't think of a single mathematical proof being anywhere close to ten million characters. For all you know, 90% of the proof could be useless, 8% would be writing out Shakespeare, and 1% abusing another bug in Lean. Humanity gets zero value from that, aside from "some bot seems to think it's 186". Unusable by anyone.
- ChrisGreenHeur 1mo ago
  You talk about modern math and worthlessness at the same time? That’s brave.
  - well_ackshually 1mo ago
    You can have your opinions about modern math, its usefulness in the world as it is, whether or not knowing if hairy balls can divide by three is actually going to be beneficial for anything but just obscure knowledge's sake. You may even say it's useless. Needless to say, a useless result that absolutely no mathematician will ever read, confirm, understand, agree with or even consider to solve their "useless" problems is an impressive waste of resources.
  - twothreeone 1mo ago
    Worthless is a pretty good description IMO in the context of what Lean is trying to achieve: "enable correct, maintainable, and formally verified code". Tens of millions of lines of LLM vomit may be many things, but it often turns out to not be correct and certainly not maintainable. Formally verified remains as a thin fig leaf covering the uncomfortable truth that formal methods only provide assurances under assumptions (your toolchain, libraries, compiler, OS, and hardware are "correct" and don't expose some exploitable flaw). It doesn't mean that it cannot improve over time, maybe the proof can be "minified" to a state where human reviewers are able to comprehend it; but as it stands there isn't really much insight or confidence to be gained from the artifact itself.
  - smokel 1mo ago
bugufu8f83 1mo ago
Based on her comments in the paper it sounds like she was aware that an AI result was coming and rushed to release her work beforehand. 240 was not a tight bound from her methods.
galaktb 1mo ago
I think this builds straight upon her method, which she said could be improved herself so...
- piker 1mo ago
  It cites to her at: [19] J. Stadlmann, On primes in arithmetic progressions and bounded gaps between many primes, Adv. Math. 468 (2025), Art. 110190. Numbered references use arXiv:2309.00425v3. Though that's not her latest paper.
  - kzrdude 1mo ago
    This one is her latest paper: [20] J. Stadlmann, Bounded gaps between primes, Forthcoming
1283751 1mo ago
With very little review: https://github.com/openai/PrimeGaps186/blob/main/formalization.yaml https://github.com/openai/PrimeGaps186/blob/main/formalizati... "No independent human semantic review. Whole-file sorry counts and a complete auxiliary-declaration audit are not established; separate declaration lint has not been run."
GPerson 1mo ago
Happened to multiple people I know.
kzrdude 1mo ago
Ok, so the rumour was exactly true: there was a withheld prime gaps improvement, that "an AI company" was holding onto until release of a model.
nilkn 1mo ago
What's just as interesting is this morning Axiom Math announced 212 and OpenAI then appears to have rushed out their 186 announcement just 1-2 hours later followed by Astra. Did they accelerate the release of Astra itself? Not necessarily, but it definitely looks like they ended up pushing much harder and faster than planned on their 186 result. X activity suggests Anthropic had a similar result as well but wasn't as fast as OpenAI in packaging it up and sharing it in response to Axiom, so they mostly just bolted onto OpenAI's messaging. The reason I think this is interesting is that Axiom is a tiny lab in comparison that wouldn't have had access to Astra at all. I'd be curious to learn how Axiom is able to effectively compete at this frontier with vastly fewer resources.
hyperpape 1mo ago
Don't think everything is just "who can produce the biggest/smallest number": https://mathstodon.xyz/@tao/117208619314517025 https://mathstodon.xyz/@tao/117208619314517025.

by Cu3PO42 1mo ago

bananaflag 1mo ago

Where did you get the link to the pdf? Was it announced somewhere?

htrp 1mo ago

https://github.com/openai/PrimeGaps186 https://github.com/openai/PrimeGaps186

dang 1mo ago
https://news.ycombinator.com/item?id=49555257 https://news.ycombinator.com/item?id=49555257
nateb2022 1mo ago
I'm surprised the OpenAI employee who pushed this didn't take the minute or two to format README.md to use GitHub-supported LaTeX (https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/writing-mathematical-expressions https://docs.github.com/en/get-started/writing-on-github/wor...) edit: my comment was on the submission for https://github.com/openai/PrimeGaps186 https://github.com/openai/PrimeGaps186 but seems to have been moved to the main Astra submission
- warkdarrior 1mo ago
  > OpenAI employee Why would you think it was an employee who did the push, instead of a random GPT agent?

well_ackshually 1mo ago

Such a result should be considered worthless: the proof is 10MB of Lean. (https://github.com/openai/PrimeGaps186 https://github.com/openai/PrimeGaps186). I can't think of a single mathematical proof being anywhere close to ten million characters. For all you know, 90% of the proof could be useless, 8% would be writing out Shakespeare, and 1% abusing another bug in Lean. Humanity gets zero value from that, aside from "some bot seems to think it's 186". Unusable by anyone.

ChrisGreenHeur 1mo ago
You talk about modern math and worthlessness at the same time? That’s brave.
- well_ackshually 1mo ago
  You can have your opinions about modern math, its usefulness in the world as it is, whether or not knowing if hairy balls can divide by three is actually going to be beneficial for anything but just obscure knowledge's sake. You may even say it's useless. Needless to say, a useless result that absolutely no mathematician will ever read, confirm, understand, agree with or even consider to solve their "useless" problems is an impressive waste of resources.
- twothreeone 1mo ago
  Worthless is a pretty good description IMO in the context of what Lean is trying to achieve: "enable correct, maintainable, and formally verified code". Tens of millions of lines of LLM vomit may be many things, but it often turns out to not be correct and certainly not maintainable. Formally verified remains as a thin fig leaf covering the uncomfortable truth that formal methods only provide assurances under assumptions (your toolchain, libraries, compiler, OS, and hardware are "correct" and don't expose some exploitable flaw). It doesn't mean that it cannot improve over time, maybe the proof can be "minified" to a state where human reviewers are able to comprehend it; but as it stands there isn't really much insight or confidence to be gained from the artifact itself.
- smokel 1mo ago

bugufu8f83 1mo ago

Based on her comments in the paper it sounds like she was aware that an AI result was coming and rushed to release her work beforehand. 240 was not a tight bound from her methods.

galaktb 1mo ago

I think this builds straight upon her method, which she said could be improved herself so...

piker 1mo ago
It cites to her at: [19] J. Stadlmann, On primes in arithmetic progressions and bounded gaps between many primes, Adv. Math. 468 (2025), Art. 110190. Numbered references use arXiv:2309.00425v3. Though that's not her latest paper.
- kzrdude 1mo ago
  This one is her latest paper: [20] J. Stadlmann, Bounded gaps between primes, Forthcoming

1283751 1mo ago

With very little review: https://github.com/openai/PrimeGaps186/blob/main/formalization.yaml https://github.com/openai/PrimeGaps186/blob/main/formalizati... "No independent human semantic review. Whole-file sorry counts and a complete auxiliary-declaration audit are not established; separate declaration lint has not been run."

GPerson 1mo ago

Happened to multiple people I know.

kzrdude 1mo ago

Ok, so the rumour was exactly true: there was a withheld prime gaps improvement, that "an AI company" was holding onto until release of a model.

nilkn 1mo ago

What's just as interesting is this morning Axiom Math announced 212 and OpenAI then appears to have rushed out their 186 announcement just 1-2 hours later followed by Astra. Did they accelerate the release of Astra itself? Not necessarily, but it definitely looks like they ended up pushing much harder and faster than planned on their 186 result. X activity suggests Anthropic had a similar result as well but wasn't as fast as OpenAI in packaging it up and sharing it in response to Axiom, so they mostly just bolted onto OpenAI's messaging. The reason I think this is interesting is that Axiom is a tiny lab in comparison that wouldn't have had access to Astra at all. I'd be curious to learn how Axiom is able to effectively compete at this frontier with vastly fewer resources.

hyperpape 1mo ago

Don't think everything is just "who can produce the biggest/smallest number": https://mathstodon.xyz/@tao/117208619314517025 https://mathstodon.xyz/@tao/117208619314517025.