we-solve (beta)

Math-568-A2 · revision r1 · on Math-568

OpenAI claim summary for Math-568

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 at unsolvedmath.com: 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.

Each manuscript supplies a universal finite bound for generalized star height on the original alphabet, with Boolean operations permitted. The successive bounds thirteen, four and three all answer this record's bounded-height question; they do not assert that every language has generalized star height at most one.

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

Manuscript

Contents
  1. The Generalized Star Height Problem
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Manuscript 2.
  6. Manuscript 3.
  7. Outline of the argument
  8. Formal verification
  9. Status caveat
  10. Sources

The Generalized Star Height Problem

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 134; 2026-09-25), the asserted result is that for an arbitrary finite alphabet and a regular language on it, a generalized expression needs at most thirteen nested star levels; In manuscript 2 (family 134; 2026-09-25), the asserted result is that every regular language has generalized star height at most four without changing its alphabet; In manuscript 3 (family 134; 2026-09-25), the asserted result is that three nested star levels suffice to express any regular language using Boolean operations and complementation in its original free monoid.

Mathematical statement of the claimed result

Manuscript 1.
A generalized regular expression may use union, concatenation, complementation and Kleene star. Its star height is the greatest nesting depth of star, and $h_{\Sigma}(L)$ is the least such height among expressions for $L$. The claim is the uniform bound \[ \forall\text{ finite }\Sigma\ \forall\text{ regular }L\subseteq\Sigma^*:\quad h_{\Sigma}(L)\le13. \] The alphabet and language may vary; the numerical bound stays fixed.
Manuscript 2.
If $h_{\Sigma}(L)$ is the minimum Kleene-star nesting depth for expressions formed using union, concatenation, complement and star, the claimed universal result is \[ \forall\text{ finite }\Sigma\ \forall\text{ regular }L\subseteq\Sigma^*:\quad h_{\Sigma}(L)\le4. \] The bound concerns generalized expressions, for which complement is permitted.
Manuscript 3.
For a finite alphabet $\Sigma$ and regular language $L$, minimize star nesting depth over expressions using union, concatenation, complementation and Kleene star. The manuscript's claimed bound is \[ h_{\Sigma}(L)\le3\qquad\text{for every such }\Sigma,L. \] Thus a single integer bounds the generalized star height across all regular languages and finite alphabets.

Outline of the argument

For manuscript 1 (family 134; 2026-09-25), finite monoid computations become affine updates recovered through split expressions. Suffix tables remember unknown prefix products, and twelve coordinated splits successively remove residual witnesses; a finite tag clock recognizes the episode endpoints.

For manuscript 2 (family 134; 2026-09-25), an affine correction hides one interval product, with each split factor of height one. Finite clocks and multiscale markers move boundaries through periodic words while limiting ambiguity, permitting exact episode reconstruction and a four-level expression.

For manuscript 3 (family 134; 2026-09-25), a prefix code of word pieces and shift tables hide individual monoid entries. Robust clocks and finite-window periodic templates verify exact ends; two splits recover the full computation, including exceptional episodes with several possible anchors.

Formal verification

For manuscript 1 (family 134; 2026-09-25), the documented Lean scope is a universal generalized star-height bound of three, which implies the paper's weaker bound thirteen; the declaration does not encode every split-construction detail.

The selected statement includes the clause used for this problem.

For manuscript 2 (family 134; 2026-09-25), the documented Lean scope is generalized star height at most three over the same alphabet, which implies the bound four stated in this manuscript.

The selected statement includes the clause used for this problem.

For manuscript 3 (family 134; 2026-09-25), OpenAI lists Lean statements for this assertion: three nested star levels suffice to express any regular language using Boolean operations and complementation in its original free monoid.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are GeneralizedStarHeight.lean.

Their named declarations include OAI.GeneralizedStarHeight.main.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources