---
id: "2026-10-06-random-3-sat-threshold-upper-bound-4-268-llm"
url: "https://postcutoff.com/e/2026-10-06-random-3-sat-threshold-upper-bound-4-268-llm/"
as_of: "2026-10-13T02:19:00+02:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 3
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 2
editor: Adam Bicz
human_review: null
version: null
---

As of: 2026-10-13 02:19 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/e/2026-10-06-random-3-sat-threshold-upper-bound-4-268-llm/

# 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'

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. The best earlier rigorous upper bound was 4.4898, and the cavity method of statistical physics predicts a threshold near 4.267. The paper says "Large language models drove the research leading to this paper" and that the proof is formalized in Lean 4. It has no independent expert review yet.

## 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

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 3.8 Flash (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [Vorobyev: An upper bound of 4.268 for the random 3-SAT satisfiability threshold (arXiv 2610.10599)](https://arxiv.org/abs/2610.10599) (arxiv.org, paper)
2. [Lean 4 formalization and certificate code (GitHub)](https://github.com/yamelton/sat-upper-4268) (github.com, code)

## Changes

- 2026-10-13 (filed): Created from the arXiv section of sweep 2026-10-13 (proof not assessed)

## Related

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-09-30: [Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help](https://postcutoff.com/e/2026-09-30-ai-assisted-conjecture-wave-summer-2026/index.md)