we-solve (beta)

CS-54-A2 · revision r1 · on CS-54

OpenAI claim summary for CS-54

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The cited theorem establishes existence of a sharp limiting threshold for each k>=3 in precisely the independent proper-clause model, but it does not identify the exact requested 3-SAT threshold value. The cited theorem establishes a computable limiting threshold via an oracle-free precision machine; the introduction explicitly says the constant is not evaluated or identified with the predicted value, whereas our target asks for the exact clause-to-variable ratio. This entry records partial support; complete coverage of the question is not established by this catalogue.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Exact satisfiability threshold for random k-SAT for small k $k = 3$
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Result 2.
  6. Outline of the argument
  7. Formal verification
  8. Status caveat
  9. Sources

Exact satisfiability threshold for random k-SAT for small k $k = 3$

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: Each fixed random clause size $k\geq3$ is claimed to have a positive finite limiting satisfiability threshold; the manuscript credits an earlier resolution by Carenini; The limiting random 3-SAT threshold is claimed computable to any requested accuracy by one finite deterministic procedure. Together they provide the following support within the scopes described below.

Mathematical statement of the claimed result

Result 1.
Fix integer $k\ge3$. Sample independent proper $k$-clauses with replacement, choosing $k$ distinct variables uniformly and each literal sign uniformly. If $P_n(m)$ denotes the satisfiability probability, the source claims a finite positive constant $\alpha_k$ with \[ \lim_{n\to\infty}P_n(\lfloor cn\rfloor)= \begin{cases}1,&0\le c<\alpha_k,\\0,&c>\alpha_k.\end{cases} \] No value at $c=\alpha_k$, or numerical formula for $\alpha_k$, is part of this theorem.
Result 2.
For uniform proper signed random 3-SAT clauses sampled independently with replacement, write $p(n,m)$ for satisfiability probability. The source asserts $\alpha_3\in(0,\infty)$ with \[ p(n,\lfloor an\rfloor)\to1\ (a<\alpha_3),\qquad p(n,\lfloor an\rfloor)\to0\ (a>\alpha_3). \] It also claims a single deterministic Turing machine that, on unary input $1^r$, halts with rational $q_r$ satisfying \[ |q_r-\alpha_3|\le2^{-r}\qquad(r\ge1). \] This machine has no oracle, advice, or noncomputable constant as input; no polynomial running-time bound is asserted. The clause-density parameter is restricted to $a\ge0$.

Outline of the argument

Replacement of shorter clauses and integrated forcing control a capped last-satisfiable index. Clause-omission pivotal estimates give concentration, while comparisons between system sizes make the normalized centers converge, producing an alternative existence proof.

Deletion bounds certify rational lower brackets, and finite hierarchical soft-pressure trials certify upper brackets. A fair enumeration of both certificate families halts at every accuracy, using existence of the limiting threshold without needing an effective finite-size convergence rate.

Formal verification

For family 235, the selected entries establish threshold existence, threshold computability, linear variance for $k\geq4$, and the earlier $O(n\log n)$ bound for $k=3$. The later linear three-clause variance improvement is not selected. The listed Comparator files are FixedClauseThreshold.lean, SATComputability.lean, SATSharpness.lean, SATVariance.lean. The inventory does not supply a named declaration for these Comparator entries. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources