Three stars suffice?

0:00Stars and complements

Regular expressions build languages, sets of words, from letters with union, concatenation and the Kleene star, which repeats a pattern any number of times. Star height counts how deeply the stars are nested. Now also allow complement: everything not in a language, over the same alphabet. Complement costs nothing in height, and it can make some stars unnecessary. Take the empty word, ab, abab, and so on. With complement they need no star at all: they are exactly the words that do not start with b, do not end with a, and contain no doubled letter. In our check, the starred and the star-free expressions agree on all 32,767 words up to length 14. But some languages do need a star, such as the words of even length over a single letter. Without complement, star height is a deep subject. Eggan tied it to the cycles of automata in 1963, and Dejean and Schützenberger showed it is unbounded, even over two letters. With complement, height zero means star-free, and Schützenberger characterized those languages in 1965 by aperiodic monoids. Henneman showed that one star suffices for languages recognized by finite abelian groups, as Pin, Straubing and Thérien recall, and they added more families. Counting a’s modulo three, the usual expression nests two stars; writing each run of b’s with a complement leaves one. But no language was known to need two, and Straubing stressed that two questions differ: is there any universal bound at all, and is that bound one?

1:36The claim

Result 134 is three OpenAI preprints, 116 pages in all, dated September 25. Each gives its own complete proof of a uniform bound: every regular language over a finite alphabet has a generalized expression over that same alphabet with at most thirteen nested stars in one paper, four in another, and three in the third. The bound does not depend on the alphabet, the language or the size of its automaton. Keeping the same alphabet matters. One companion paper notes that, by results of Pin, Straubing and Thérien, if height bounds survived replacing letters by whole words, one star would already suffice; so the construction never adds letters. What is not claimed: that three is optimal. No language is shown to need two stars, so the true worst case is one, two or three. The expressions can be enormous: the papers bound only the nesting, not the size of the expression or the time to build it. OpenAI published a Lean formalization of the bound of three, which implies the other two: 37 files and about 12,000 lines, not counting Mathlib. We have not run the Lean check.

2:46How the proof goes

All three proofs start from a finite monoid. Run an automaton on a word and record the resulting map from states to states. These maps form a finite monoid, and the language is a union of the sets of words with a given product, so it suffices to describe each of those sets. The proofs cut each word into episodes, pieces from a prefix code so that the cutting is unique. An episode ends by a local rule: a fixed distance after a marker pattern, or else a fixed distance after a periodic stretch first breaks. So each episode is bounded data, at most one long periodic run, and a bounded tail. Powers of a monoid element eventually repeat, so the run lengths that matter form an eventually periodic set, written with one star. That is the first star. To string episodes together, the proof cuts an episode in two: a prefix test for the incoming state and a suffix test for the outgoing one. One star repeats this along the word, passing over skipped episodes. Each split costs one star. The trouble is that a prefix and a suffix are separate pieces of a concatenation: the only thing they share is where the cut falls. So the proof uses a clock. The prefix measures one distance to the cut and the suffix another, and once an end guard makes both sides agree on where the episode ends, their sum is fixed by the episode itself. The sets are built so that either the two sides agree, or there is exactly one disagreeing pair, which an affine correction absorbs. Corrections are free: comparing the run from the real input with a run from zero cancels the translation, using only unions and intersections. The remaining obstacle is the one block of the word that straddles the cut, which neither side can read in full. A shift table handles it: with one tuple length that works for every table of maps, a fixed correction is chosen for each table, such that for every tuple and every input, some coordinate can change without changing the result. Then the hidden block never needs to be known. For long enough tuples, a random correction works with positive probability, by the Erdős–Lovász local lemma. In our check, in the smallest nontrivial case, two symbols and a one-bit state, length three works for every table, while lengths one and two fail for some; the paper’s general estimate would need length thirteen. With these tools, the three-star paper needs only two splits. The outer split, over all episodes, skips those where the clock or the marker searches fail. The inner split, over those, places copies of the information at carefully spaced positions so that one copy can always be decoded. Periodic runs give the first star, the inner split the second, and the outer split the third. The thirteen-star paper used twelve splits, and the four-star paper used three.

5:40Where it stands

The three preprints are not peer reviewed and have not been revised. The Lean formalization covers the bound of three; we have not run it. None of these papers is among those OSVerify reviewed, and we have seen no expert review. If it holds, three nested stars, together with complement over the same alphabet, are enough for every regular language, answering the uniform boundedness question. Whether one star always suffices is still open, so the answer now is one, two or three.