we-solve (beta)

Math-2921 · mathematics · Probability

Oracle-free computation of the limiting random 3-SAT threshold

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For independent proper uniformly signed random 3-clauses, is there a limiting sharp density $\alpha _3$ and one deterministic finite Turing machine that, on every unary precision input $1^r$, halts with a rational $q_r$ satisfying $|q_r-\alpha _3|\leq 2^{-r}$, using no oracle, advice or noncomputable parameter?

Short English statement

For independent proper uniformly signed random 3-clauses, is there a limiting sharp density $\alpha _3$ and one deterministic finite Turing machine that, on every unary precision input $1^r$, halts with a rational $q_r$ satisfying $|q_r-\alpha _3|\leq 2^{-r}$, using no oracle, advice or noncomputable parameter?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2921-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2921

The limiting random 3-SAT threshold is claimed computable to any requested accuracy by one finite deterministic procedure. The question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.

Oracle-free computation of the limiting random 3-SAT threshold

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The limiting random 3-SAT threshold is claimed computable to any requested accuracy by one finite deterministic procedure.

Mathematical statement of the claimed result

Result 1.
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

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

Go to contribution →