AI Proved What?

Episode 005, October 2026

Not a fraction

Catalan’s constant is irrational

Covers result 005 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

Play Episode 005: Not a fraction. Catalan’s constant, 1 − 1/9 + 1/25 − 1/49 + …, beside a chessboard tiled with dominoes and the value G = 0.9159655941…

7:02. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Is this number a fraction?
  2. 0:43Catalan’s constant
  3. 1:19Its famous relatives
  4. 2:20How to prove a number is irrational
  5. 3:07A determinant instead
  6. 3:50The squeeze
  7. 4:44Ruling out zero
  8. 5:23The Lean proof
  9. 6:13Why it matters, and the caveats

The claim, in plain words

Catalan’s constant is the number G = 1 − 1/9 + 1/25 − 1/49 + ⋯ = 0.9159655941…, the alternating sum of the reciprocals of the odd squares. It turns up in many places: it is the area under arctan(x)/x from 0 to 1, a quarter of the volume of the regular ideal octahedron in hyperbolic space (and of the space around the Whitehead link), and the rate, G/π per square, at which the number of domino tilings of a large board grows. It is named after Eugène Catalan, who published a memoir on it in 1865.

Its relatives are famous. With plain odd numbers instead of odd squares the same alternating sum is π/4 (Leibniz), and with any odd power it is a rational multiple of a power of π. The even powers are different, and no formula for G in terms of π is known. Whether G is irrational was a long-standing open question: in 2013 it was called “arguably the most basic constant whose irrationality and transcendence (though strongly suspected) remain unproven.”

Result 005 claims the answer: G is irrational. It is not a ratio of two whole numbers.

What it doesn’t claim

The paper proves irrationality and nothing quantitative: it says a bound on how well fractions can approximate G (an irrationality measure) “would require additional control of rational approximations.” It says nothing about whether G is transcendental, and nothing about the next even values such as 1 − 1/34 + 1/54 − ⋯. Its only further claims are corollaries in geometry: the volume of the Whitehead link complement (4G) and every volume of an orientable arithmetic hyperbolic 3-orbifold defined over ℚ(i), which is a rational multiple of G, are irrational.

Where it stands

Posted as a preprint
OpenAI, dated September 24, 2026; released October 6, 2026
Peer reviewed
Not yet
Checked in Lean
OpenAI published a Lean proof of the main theorem (scope note); we have not run the check

Last checked October 19, 2026. The claim has not been withdrawn, and the paper was unchanged in the release’s October 7 update. A separate claimed proof by Zhi-Wei Sun (arXiv:2609.04176, posted September 3, 2026) has a reported gap: a note by Dane Wachs (arXiv:2609.22339) finds that a key estimate fails in exact tests, much of the discrepancy coming from the prime 2. OpenAI’s paper cites Sun’s preprint and says no result from it is used.

How the proof goes

  1. Why the classic method stalled. If G = p/q, every combination AG − B with whole numbers A, B is zero or at least 1/q in size, so nonzero combinations shrinking to zero would prove irrationality. That is Apéry’s route for ζ(3). For G, known approximations converge quickly, but after clearing denominators the combinations do not go to zero (Zudilin, 2003).
  2. A determinant instead. The paper builds a determinant ΔN of size 48N. Each entry comes from integrals and equals a rational number plus a rational multiple of G plus a rational multiple of ζ(2). The rows are built from Chebyshev polynomials chosen so that every ζ(2) part cancels exactly. So if G were rational, every ΔN would be rational.
  3. The floor. A nonzero rational number is at least 1 over its denominator. Bounding the denominator one prime at a time (the prime 2 separately; the odd primes through a loss curve summed with the prime number theorem) gives, if G were rational, log |ΔN|/(48N)² − ½ log 2 ≥ −2.29081 in the long run.
  4. The ceiling. With no assumption, Andréief’s identity and Cauchy’s determinant write ΔN as a large integral. Logarithmic-potential estimates, certified by explicit rational numbers, give the same quantity ≤ −2.290939875 in the long run. The ceiling is below the floor by about 0.00013, which is a contradiction for large enough N.
  5. Ruling out zero. The floor needs ΔN ≠ 0. Assuming G is rational, the paper shows that for every large prime p, Δp is not zero: modulo p the matrix reduces to blocks built from three fixed 48 × 48 matrices, whose determinants are certified nonzero by Gaussian elimination modulo 101 (144 nonzero pivots).

The Lean statement

theorem catalan_irrational :
    Irrational (∑' j : ℕ,
      (-1 : ℝ) ^ j / ((2 * j + 1 : ℕ) : ℝ) ^ 2)

This is the challenge statement that OpenAI’s setup checks with the Comparator tool. A passing check guarantees that the proof proves exactly this statement, using only Lean’s standard axioms (propext, Quot.sound, Classical.choice), and that Lean’s kernel accepts it. The proof itself is 981 files, 573,816 lines; about 69% of the lines write out the mod-101 elimination step by step. Its last step mirrors the paper: suppose the sum is a rational z, combine the floor and the ceiling along large primes, and let linarith find the contradiction. A search of those files found no sorry and no new axioms, but a search is not a substitute for running the check, and we have not run it. OpenAI says its papers and proof files were produced by an internal AI model; its catalog of formal proofs gives their review status as “unchecked” and does not yet list this proof.

The numbers in the video

  • G = 0.91596559417721901505…; partial sums 1, 0.889, 0.929, 0.908, …; ∫01 arctan(x)/x dx = G; 4G = 3.66386…; G/3 = 0.30532… (mpmath).
  • The 8 × 8 board has 12,988,816 domino tilings (Kasteleyn’s product formula). log(tilings)/area is 0.256 for 8 × 8, 0.289 for 100 × 100 and 0.291 for 400 × 400, tending to G/π = 0.29156…
  • The two starting integrals equal 4G and π²/4 = (3/2)ζ(2); the ζ(2) parts cancel for all 48 rows at N = 1 (checked exactly).
  • The odd-prime loss curve has area 8609/2. The floor is −8609/4608 − (1/2 + 505/4608) log 2 = −2.2908096…; the ceiling is −2.290939875.
  • From the paper’s recipe we rebuilt the fixed 49 × 48 rational matrix and reran the elimination modulo 101. All 144 pivots, and the two row swaps, match the paper’s table.
  • The loss curve, certificate digits and pivots on screen are copied from the paper.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00Is this number a fraction?

How many ways can you cover a chessboard with dominoes? 12,988,816. On bigger boards the count grows exponentially with the area, and the growth rate is G divided by π, where G is about 0.916. G is Catalan’s constant. 1 − 1/9 + 1/25 − 1/49, and so on, over the odd squares. Is it a fraction? Nobody could prove it either way. Result 005 in OpenAI’s math repository claims the answer: no. G is irrational. And the claim comes with a proof in Lean, a language for computer-checked mathematics.

0:43Catalan’s constant

The signs alternate, so the running totals zig-zag. One. Then about 0.89. Then 0.93, closing in on 0.915966. The number turns up all over mathematics. It’s the area under arctan(x)/x from 0 to 1. Four times G is the volume of the perfectly symmetric ideal octahedron in hyperbolic space, and of the space around a famous pair of linked loops, the Whitehead link. It’s named after Eugène Catalan, who published a memoir on it in 1865.

1:19Its famous relatives

Its relatives are famous. Use plain odd numbers instead of odd squares, and you get Leibniz’s series, 1 − 1/3 + 1/5, which equals π/4. With odd cubes you get π³/32. Every odd power gives a fraction times a power of π. The even powers are the mystery, and G is the first of them. No formula in terms of π is known. Compare ζ(2), 1 + 1/4 + 1/9 and so on. Euler showed it equals π²/6, which is irrational. ζ(3) was proved irrational by Apéry in the late 1970s. For G, the best results were about whole families. Rivoal and Zudilin proved in 2003 that infinitely many of these even values are irrational. Later work showed that at least one of the first five is. But no one could say which one. In 2013, G was called arguably the most basic constant whose irrationality remains unproven.

2:20How to prove a number is irrational

Here’s the classic tool. Suppose G were a fraction, p/q. Take any whole numbers A and B. Then A·G − B is a whole number divided by q. So it’s either zero, or at least 1/q in size. It can’t be tiny without being zero. So if you can find whole numbers where AG − B is never zero, but shrinks toward zero, G cannot be a fraction. That’s how Apéry’s proof works. For G, mathematicians found fractions B/A that approach it very fast. The catch is the denominators. To get whole numbers you multiply by A, and A grows faster than the error shrinks. In Zudilin’s construction, the combinations do not go to zero. For decades, that was the wall.

3:07A determinant instead

The new proof changes the object. Instead of one combination, it builds a big square grid of numbers and takes its determinant, called Δ_N. The grid is 48N rows by 48N columns. Each entry comes from an integral, and each integral works out to a fraction, plus a fraction times G, plus a fraction times ζ(2). The rows are built from Chebyshev polynomials, chosen so that every ζ(2) part cancels exactly. We checked that cancellation for all 48 rows when N = 1. So if G were a fraction, every entry would be a fraction, and so would the determinant. The proof then squeezes that fraction from both sides.

3:50The squeeze

From below. A nonzero fraction can’t be smaller than 1 over its denominator. So the paper limits the denominator, one prime at a time. The prime 2 gets its own estimate. The odd primes follow a loss curve, and the prime number theorem adds them all up. On a suitably normalized log scale, that gives a floor. If G were a fraction, this measure could never sink below −2.29081, in the long run. From above, with no assumption at all, the paper writes the determinant as a giant integral and bounds it. Explicit rational numbers certify the result: a ceiling at about −2.29094. The ceiling sits below the floor, by about one ten-thousandth. No fraction can do both. The gap is so thin that the squeeze only works for very large grids. In a proof, that’s fine.

4:44Ruling out zero

Well, almost. One loophole is left. Zero is a fraction too, and a zero determinant would slip under the floor. So the paper shows that, if G were a fraction, the determinant couldn’t be zero whenever N is a large prime p. Working modulo p, the huge grid collapses into copies of three fixed 48 × 48 matrices. If those three are invertible, so is the giant one. The paper certifies them by elimination modulo 101: 144 pivots, and none of them is zero. We reran that elimination from the paper’s recipe. Every pivot matched.

5:23The Lean proof

Now the computer proof. Here’s the statement in Lean: the sum of (−1)^j/(2j + 1)² is irrational. Behind it sit about 980 files, more than half a million lines. The last step reads like the paper. Suppose the sum equals a rational number z. Take the floor and the ceiling along large primes, and let arithmetic find the contradiction. OpenAI set it up for a checking tool called Comparator. A passing check guarantees that this exact statement is proved, using only Lean’s usual axioms. OpenAI says its papers and proof files were produced by an internal AI model. Its catalog of formal proofs marks their review status as unchecked, and doesn’t list this one yet. And we haven’t run the check ourselves.

6:13Why it matters, and the caveats

If it holds, geometry gets answers too. The volume around the Whitehead link is 4G, so it’s irrational. So is every volume in a whole family of hyperbolic shapes built from the Gaussian integers. The caveats. This is a preprint, and it hasn’t been peer reviewed. The main theorem is formalized in Lean, but we haven’t run the check. A different claimed proof, posted on September 3, has been questioned: a note reports a gap, much of it at the prime 2. This paper doesn’t use it. And questions remain. Is G transcendental? How closely can fractions approximate it? Is the next even value irrational? For now: Catalan’s constant is not a fraction, if the proof holds. And this time, a computer can check it.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.