we-solve (beta)

Math-2902 · mathematics · Probability

A limiting density threshold for every fixed random clause size

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For each fixed $k\geq 3$, do independent uniformly signed k-clauses using k distinct variables, sampled with replacement on n variables, have a constant $\alpha _k\in (0,infinity)$ such that satisfiability probability at floor(cn) clauses tends to one for every $c<\alpha _k$ and to zero for every $c>\alpha _k$?

Short English statement

For each fixed $k\geq 3$, do independent uniformly signed k-clauses using k distinct variables, sampled with replacement on n variables, have a constant $\alpha _k\in (0,infinity)$ such that satisfiability probability at floor(cn) clauses tends to one for every $c<\alpha _k$ and to zero for every $c>\alpha _k$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2902

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 question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.

A limiting density threshold for every fixed random clause size

OpenAI's claim

OpenAI presents a proof in the selected manuscript. 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.

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.

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.

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 →