Preprint claims a 4.268 upper bound for the random 3-SAT threshold, down from 4.4898, with a Lean 4 proof; ‘large language models drove the research’
Awaiting review
The takeaway
Fedor Vorobyev’s arXiv preprint 2610.10599 (Oct 6, 2026) claims that a random 3-SAT formula with 4.268n clauses is unsatisfiable with high probability.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 13 October 2026
Your AI and this story
- GPT-6 Astra159 days after its cutoff
- Claude Opus 5.598 days after its cutoff
- Gemini 3.8 Flash189 days after its cutoff
- Grok 4.7128 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 98 days before it.
Key facts
- Claim (abstract): ‘a random 3-SAT formula with n variables and ⌊4.268n⌋ clauses is unsatisfiable with high probability’
- Earlier state, as the abstract gives it: ‘successive upper bounds reached 4.4898 in the work of Díaz, Kirousis, Mitsche, and Pérez-Giménez, while the cavity method predicts a value near 4.267’
- Method (abstract): builds on interpolation methods, ‘including the energetic approach of Achlioptas and Menchaca-Méndez’; bounds the smallest number of clauses any assignment must violate by comparison with a simpler system of constraints on single variables; ends in a finite calculation checked in exact rational arithmetic
- AI disclosure (Section 9, verbatim): ‘Large language models drove the research leading to this paper. Their contribution included developing the mathematical argument, generating and revising the Lean formalization and numerical code, and drafting and revising the manuscript. The author directed the work and worked with the models to improve the explanations and presentation.’ The models are not named
- Verification statement (verbatim): ‘Lean checks the proof of the formal theorem; the correspondence between the formal definitions and the intended model, and between the formal proof and this exposition, requires human inspection. We do not claim an independent human verification of every step.’
- 16 pages, single author; Lean sources and certificate code at github.com/yamelton/sat-upper-4268 (Apache-2.0), archived on Zenodo (doi 10.5281/zenodo.23120101)
- Reactions: none found. A Hacker News search on Oct 13 returned no thread; X was not searched in this quick run
What happened
In random 3-SAT, each clause picks three of n variables at random. As the ratio of clauses to variables grows, formulas go from almost always satisfiable to almost always unsatisfiable. Physicists’ cavity method puts the switch near 4.267, but proofs lag: the rigorous upper bound stood at 4.4898.
Fedor Vorobyev’s preprint claims 4.268, a hair above the predicted value. The argument compares the random formula with a simpler system by interpolation and reduces the bound to a finite computation with rational numbers. The author states that language models developed the mathematics, wrote the Lean 4 formalization and drafted the paper, and that he directed them.
Why it matters
If it holds, this closes almost all of the gap between what is proved and what physics predicts for one of the best-known problems on random constraint satisfaction. It is also a test of a pattern that is becoming common: a single author, unnamed models, and a Lean proof in place of peer review.
The caution is the paper’s own. Lean certifies the formal theorem, and a human has to confirm that the formal statement is the real random 3-SAT model. Nobody outside has done that in public yet. The author’s background was not checked, and the models used are not named. Treat the result as a claim until specialists respond.
What is disputed or not yet verified
| Verification | Lean 4 formalization of the main theorem by the author; unrefereed preprint, no independent check of the formal statement against the intended model |
|---|
Sources
2 sources from 2 sites. Numbers match the chips in the text.
2 sources: 2 primary
Primary
Changes
- Filed from the arXiv section of sweep 2026-10-13 (proof not assessed)