Odlyzko–Poonen conjecture (1993) proved unconditionally
‘The proofs are due to GPT-6 Astra’, which also wrote a 22,000-line Lean formalisation
Result confirmed
Importance: major (4 of 5)The takeaway
Constantin Kogler posted an unconditional proof of the Odlyzko–Poonen conjecture: a random monic 0/1 polynomial with constant term 1 is irreducible over Q with probability tending to 1 (arXiv 2609.26771, 22 Sep 2026).
Status
- Claim
Result confirmed
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 7 October 2026
Your AI and this story
- GPT-6 Astra145 days after its cutoff
- Claude Opus 5.584 days after its cutoff
- Gemini 4 Hydrogen175 days after its cutoff
- Grok 4.7114 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 84 days before it.
Key facts
- Conjecture: Odlyzko and Poonen (1993); Konyagin (1999) gave a c/log n lower bound; Breuillard–Varjú (2019) proved it under GRH; Bary-Soroker–Koukoulopoulos–Kozma (2023) handled coefficients from at least 35 consecutive integers
- New: P(P_n irreducible) → 1 unconditionally, with P(reducible) = sqrt(2/(πn)) + O(1/n)
- Machine Contribution Statement: ‘The proofs are due to GPT-6 Astra. The author rewrote and checked the arguments’; first found on 14 Sep 2026, after the model had proved a related result on Bernoulli convolutions (first under GRH, then unconditionally)
- ‘GPT-6 Astra formalized all results from this paper and all necessary results from previous work. The formalization took around 30 hours and around 22’000 lines of code were written’ (repository ckkogler/odlyzko-poonen-lean)
- Kogler thanks Emmanuel Breuillard ‘for checking the proof’, and thanks Breuillard and Péter Varjú for help with the writing
What happened
While studying Bernoulli convolutions with GPT-6 Astra, Kogler saw the model remove a GRH assumption from a related result. He then asked it to try the Odlyzko–Poonen conjecture. The model produced a proof and formalised it together with all the prior results it needed.
Why it matters
The unconditional case had stayed open after Breuillard and Varjú’s conditional proof in 2019. The paper assigns the mathematics fully to the model and includes both a machine-checked proof and a check by a leading expert, which is unusually complete verification for an AI result.
Sources
2 sources from 2 sites. Numbers match the chips in the text.
2 sources: 2 primary
Primary
Changes
- Science block: short label for the open-problems table
- Filed