we-solve (beta)

Math-2604-A1 · revision r1 · on Math-2604

OpenAI claim summary for Math-2604

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 algorithmic theorem matches every sufficiently large even order at each fixed degree, with deterministic polynomial bit complexity. Its strict nontrivial eigenvalue inequalities imply the requested non-strict Ramanujan condition as well as connectedness and nonbipartiteness.

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

Manuscript

Contents
  1. Deterministic nonbipartite Ramanujan graphs in every fixed degree
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Deterministic nonbipartite Ramanujan graphs in every fixed degree

OpenAI's claim

Deterministic nonbipartite Ramanujan graphs: For each fixed $d\ge3$, the claimed deterministic polynomial-time construction gives a simple nonbipartite $d$-regular graph at every sufficiently large even order. All nonconstant eigenvalues lie strictly inside the tree spectral interval.

Mathematical statement of the claimed result

Mathematical claim 1.
For every fixed integer $d\ge3$ there are $n_0(d),k_d$ and a deterministic algorithm which, on every even $n\ge n_0(d)$, outputs an adjacency list using $O_d(n^{k_d})$ bit operations. Its $n$-vertex graph $G$ is simple and has degree $d$ at every vertex. The asserted adjacency eigenvalue condition is \[-2\sqrt{d-1}<\lambda<2\sqrt{d-1}\quad\text{for every eigenvalue of }A_G|_{\mathbf1^\perp}.\] These strict inequalities imply that $G$ is connected and nonbipartite, and in particular imply the requested non-strict Ramanujan bound.

Outline of the argument

Deterministic nonbipartite Ramanujan graphs: Partial stub pairings are assigned matrix pencils whose inverses admit path expansions. Resolving one pair has an explicit low-rank update, allowing positivity to be maintained for both spectral signs. The exposure rule is implemented with finite arithmetic and simplicity constraints, producing a complete pairing and its adjacency list with the required two-sided spectral control.

Formal verification

Deterministic nonbipartite Ramanujan graphs: The pinned catalogue lists no Lean formalization for this result.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources