Theoretical computer science · Result 134

Generalized star height at most three

3 papersLean

Every regular language over a finite alphabet has a generalized regular expression with at most three nested Kleene stars, allowing union, concatenation and complement over the same alphabet. This establishes an absolute bound independent of automaton size, resolving the uniform-boundedness version of the generalized star-height problem.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Finite Monoid Computations and a Uniform Generalized Star-Height Bound

OpenAI · September 25, 2026

Every regular language over a finite alphabet has a generalized regular expression of star height at most thirteen over that same alphabet. We prove this uniform bound by representing finite monoid computations as affine updates and recovering them through twelve successive split constructions.

Read PDF Download Source

Cite

@misc{OAI:Finite-Monoid-Computations-and-a-Uniform-Generalized-Star-Height-Bound-September-25-2026,
  author = {{OpenAI}},
  title = {{Finite Monoid Computations and a Uniform Generalized Star-Height Bound}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Finite-Monoid-Computations-and-a-Uniform-Generalized-Star-Height-Bound-September-25-2026/Finite-Monoid-Computations-and-a-Uniform-Generalized-Star-Height-Bound-September-25-2026.pdf}{OAI:Finite-Monoid-Computations-and-a-Uniform-Generalized-Star-Height-Bound-September-25-2026}},
  year = {2026}
}

Generalized Star Height at Most Four

OpenAI · September 25, 2026

Every regular language over a finite alphabet has generalized star height at most four over that same alphabet. We give a complete construction using an affine correction that hides one interval product, a finite clock, and several scales for moving boundaries through periodic words.

Read PDF Download Source

Cite

@misc{OAI:Generalized-Star-Height-at-Most-Four-September-25-2026,
  author = {{OpenAI}},
  title = {{Generalized Star Height at Most Four}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Generalized-Star-Height-at-Most-Four-September-25-2026/Generalized-Star-Height-at-Most-Four-September-25-2026.pdf}{OAI:Generalized-Star-Height-at-Most-Four-September-25-2026}},
  year = {2026}
}

Generalized Star Height at Most Three

OpenAI · September 25, 2026

Every regular language over a finite alphabet has generalized star height at most three, with complement taken in the same free monoid. We express finite-monoid computations using a prefix code of word pieces.

Read PDF Download Source

Cite

@misc{OAI:Generalized-Star-Height-at-Most-Three-September-25-2026,
  author = {{OpenAI}},
  title = {{Generalized Star Height at Most Three}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Generalized-Star-Height-at-Most-Three-September-25-2026/article.pdf}{OAI:Generalized-Star-Height-at-Most-Three-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Generalized star height measures the nesting of Kleene stars in regular expressions that also allow Boolean operations. The formalization proves that every regular language over a finite alphabet has a generalized expression over the same alphabet of star height at most three. This is stronger than the bound of thirteen in the accompanying finite-monoid paper. The selected statement asserts the uniform expression bound, without separately encoding every construction step of that paper.

The formalization proves that every regular language over a finite alphabet has a generalized regular expression over that same alphabet with star height at most three. Generalized expressions allow Boolean operations as well as concatenation and Kleene star. The bound of three implies the accompanying paper's bound of four; the selected statement concerns the expression bound itself.

Generalized star height measures the nesting of Kleene stars in regular expressions that also allow Boolean operations. The formalization proves that every regular language over a finite alphabet has a generalized regular expression over that same alphabet of star height at most three. Complements are taken in the same free monoid. This is the paper's uniform bound.

Comparator links

Result	Comparator statement
Uniform generalized star-height bound of three	GeneralizedStarHeight.lean
Generalized star height at most three	GeneralizedStarHeight.lean

Scope note on GitHub →