Only so lucky

0:00How close can fractions get?

22/7 is a famous fraction for pi. 355/113 is far better: it misses by less than 3 ten-millionths. How close can fractions get to pi? There’s a natural yardstick. For any irrational number, infinitely many fractions p/q come within 1/q² of it. So the real question is whether pi allows much better than that, infinitely often. The irrationality exponent of pi measures exactly this, and mathematicians expected it to be 2. Result 017 in OpenAI’s math repository claims to prove it, and, as a consequence, that a notorious series converges.

0:43The exponent

Here is the definition. Pi’s irrationality exponent is the largest power ν, strictly the supremum, such that infinitely many fractions come within 1/q^ν. Every irrational number has exponent at least 2, and almost every real number has exactly 2. Exponent 2 allows occasional lucky fractions, but they can’t get too lucky. The continued fraction of pi shows where luck comes from: 3; 7, 15, 1, 292. That 292 is why 355/113 is so good. It beats the 1/q² yardstick about three hundred times over. The claim, exponent 2, says that for any power bigger than 2, past some point, no fraction comes that close. It still allows large terms in the continued fraction, as long as they grow more slowly than any power of the denominators.

1:37What was known

For irrational algebraic numbers, like the cube root of two, Klaus Roth proved exponent 2 in 1955, work recognized with a Fields Medal. But pi is not algebraic, so Roth’s theorem says nothing about it. For pi, the best results were upper bounds. Kurt Mahler proved 42 in 1953. Then 20, 8, 7.6, and in 2020 Doron Zeilberger and Wadim Zudilin reached 7.103. The claim jumps straight to 2, the lowest possible value.

2:12The Flint–Hills series

Now the series. Add up 1/(n³ sin² n), for n = 1, 2, 3, and so on. Whenever n is close to a multiple of pi, sin n is tiny, and the term spikes. At n = 355, a single term is about 24.6. Up to a million, the sum is about 30.3. But does it converge? A future spike could be huge, if pi had fractions that were too good. Max Alekseyev showed in 2011 that convergence would force pi’s exponent to be at most 5/2, and later work showed that below 5/2 is enough. The claim gives 2, so the series converges.

2:53How the proof goes

The proof is an interpolation determinant argument, with one idea from Roth. Suppose pi had infinitely many fractions better than 1/q^ν, for some ν above 2. Pick several of them, with denominators spread far apart, as Roth did. Each fraction gives an approximation to 2πi, the period of the logarithm. The paper proves that polynomials in the exponential and logarithm can match any prescribed values for many Taylor coefficients at once. So a square matrix of those coefficients has a nonzero determinant. Being nonzero, with controlled denominators, it can’t be too small. But because the fractions are so close to the true periods, an analytic estimate forces the same determinant to be smaller still. The two estimates collide, so only finitely many such fractions exist.

3:46Lean, and the caveats

OpenAI also published a Lean proof of the main theorem: for every ν above 2, some threshold Q exists past which every fraction misses pi by at least 1/q^ν, and the exponent equals 2. It runs to about 95,000 lines. It isn’t in OpenAI’s formalization catalog yet, and we haven’t run the check. The Flint–Hills consequence is proved in the same Lean files, but it isn’t part of the official statement. This is a preprint, not peer reviewed. The threshold Q is not computed, and the method can’t compute it, so the result gives no explicit bound. And it doesn’t say whether pi’s continued fraction has bounded terms. That remains open. 355/113 is lucky. Pi only gets so lucky. If the proof holds.