A number can be easy to calculate and maddeningly difficult to understand. Catalan’s constant fits that description perfectly. Its defining series is simple enough to write on a napkin, yet deciding whether the result is a fraction resisted generations of mathematical work.
OpenAI’s manuscript dated September 24, 2026, claims a proof of its irrationality. The accompanying repository documentation states that a Lean formalization covers the headline assertion. Those are concrete developments, although documentation alone should not be confused with an independently reproduced proof audit.
The interesting story lies inside the argument. Earlier approximations kept running into a denominator problem. The new construction attacks that obstacle with carefully engineered determinants, exact arithmetic, and competing bounds that cannot both hold if the number is rational.
Understanding that mechanism gives readers something more useful than another announcement that AI has solved something difficult.
Table of Contents
1. What Is Catalan’s Constant? Definition, Formula, and Value
The constant is defined by the alternating sum of reciprocal odd squares:
[ G=\sum_{n=0}^{\infty}\frac{(-1)^n}{(2n+1)^2} =1-\frac19+\frac1{25}-\frac1{49}+\cdots. ]
Numerically, (G) is approximately (0.915965594177219). It equals (\beta(2)), where (\beta) is the Dirichlet beta function, and is also written (L(2,\chi_{-4})).
Catalan’s Constant: Key Facts and the Irrationality Claim
| Key Fact | What It Means |
|---|---|
| Symbol | Usually written as G |
| Defining Series | Alternating reciprocals of odd squares |
| Approximate Value | 0.915965594177219 |
| Research Problem | Whether G can equal a ratio of integers |
| New Manuscript | OpenAI, September 24, 2026 |
| Claimed Result | Irrationality of this specific constant |
| Formalization Scope | The repository reports the headline assertion in Lean |
The name creates avoidable confusion. Catalan numbers form an integer sequence used in combinatorics. Catalan’s conjecture concerns consecutive perfect powers and is now known as Mihăilescu’s theorem. Neither is the irrationality problem discussed here.
2. Is Catalan’s Constant Irrational? What the Paper Establishes
The manuscript answers yes through a proof by contradiction. It assumes (G) is rational and derives incompatible estimates for a sequence of nonzero determinants.
For readers checking the result’s status, several kinds of evidence need to remain distinct:
Catalan’s Constant Proof: What the Evidence Establishes
| Evidence | What It Supports | What It Does Not Establish Alone |
|---|---|---|
| Written Manuscript | A proposed mathematical derivation | Independent acceptance of every step |
| Exact Finite Certificates | Specific arithmetic and inequality checks | The full infinite argument without its surrounding lemmas |
| Lean Scope Documentation | The author’s description of the formalized theorem | An independently reproduced build and audit |
| Expert Commentary | Assessment of methods and mathematical interest | A complete verification unless explicitly supplied |
This distinction helps avoid two unhelpful reactions: accepting a headline without examining its evidence, or dismissing a formalized result because its prose is difficult. Correctness, readability, and novelty deserve separate consideration.
3. What Mathematicians Had Proved Before This Paper
Previous research had made substantial progress around the target. Rivoal and Zudilin showed that infinitely many even beta values are irrational, with at least one irrational value among (\beta(2),\beta(4),\ldots,\beta(14)). Later work narrowed that finite collection, eventually reaching the five values through (\beta(10)).
But a guarantee that one member of a group is irrational does not identify which member. The smallest value, (\beta(2)), could still escape the conclusion.
Apéry’s irrationality proof for (\zeta(3)) offered an influential model: construct rational approximations whose errors shrink fast enough to survive denominator clearing. Related recurrences, continued fractions, and integral formulas were developed for (G), but the same arithmetic payoff did not follow.
The manuscript also distinguishes nearby successes. A result for a character of conductor 3 does not automatically settle the conductor-4 constant here. Likewise, irrationality of a 2-adic analogue does not transfer directly to the real number. Similar notation can conceal a different arithmetic problem.
These earlier results are essential context. They explain both why researchers expected progress and why the final target remained stubborn. The missing ingredient was not another decimal calculation. It was a construction whose analytic accuracy and arithmetic structure could finally cooperate strongly enough to isolate this one value.
4. Why Proving Irrationality Was So Difficult
Suppose fractions (p_n/q_n) approach (G). The relevant quantity is often
[ \left|q_nG-p_n\right| =q_n\left|G-\frac{p_n}{q_n}\right|. ]
Multiplication by (q_n) can erase the apparent improvement. An error of (10^{-100}) looks spectacular until its denominator is (10^{150}). The scaled error would then be (10^{50}), hardly a quantity approaching zero.
Why does that matter? If (G=a/b) were rational, every nonzero expression (q_nG-p_n), with integer (p_n,q_n), would have absolute value at least (1/b). Producing nonzero expressions tending to zero would contradict that fixed lower bound.
The challenge is therefore precise: make the error decay faster than the arithmetic cost grows. The denominator is part of the proof, not an administrative detail.
Numerical digits cannot settle the question either. Any finite decimal prefix can belong to both rational and irrational numbers. A continued-fraction representation also needs additional arguments establishing the relevant arithmetic behavior.
An infinite Euler product is no shortcut. Infinite products of rational factors can have rational limits. For example,
[ \prod_{n=2}^{\infty}\left(1-\frac1{n^2}\right)=\frac12. ]
The finite products telescope to ((m+1)/(2m)), making the rational limit explicit. Infinitely many factors do not force irrationality.
5. The New Strategy: Two Bounds That Cannot Coexist
The OpenAI Catalan’s constant proof uses determinants (\Delta_N) of matrices with (48N) rows and columns. A determinant combines all the matrix entries into a single number, preserving interactions that separate entrywise estimates can miss.
Here the entries come from integrals, called moments, built using two elementary kernels and specially selected polynomials.
Under the assumption (G\in\mathbb Q), the construction makes each determinant rational. Arithmetic then limits how small a nonzero determinant can be, because its denominator is controlled. Independently, an integral representation limits how large its absolute value can be.
The goal is to make the analytic upper bound fall below the arithmetic lower bound as the matrices grow.
This strategy has earlier precedents. The manuscript’s contribution is the particular construction and estimates that make it work for (G). Simply replacing an approximation with a matrix would not solve the denominator problem. Every part of the matrix has to earn its place.
For developers, the construction resembles designing an intermediate representation that exposes properties hidden in the original input. The determinant packages many relations together, allowing shared cancellation and divisibility to influence the final quantity. That analogy explains the design choice, although the actual proof still depends on the specific algebra and estimates.
6. The Crucial Cancellation: Removing an Extra Constant
Initially, the moment formulas involve rational combinations of three quantities: (1), (G), and (\zeta(2)). The last equals (\pi^2/6).
That extra term matters. Assuming (G) rational would not make entries rational if a nonzero (\zeta(2)) contribution remained.
The paper chooses polynomial rows whose associated expressions agree through many initial Taylor coefficients. This carefully imposed agreement cancels the unwanted term in every entry. Chebyshev polynomials also supply integer coefficients and useful divisibility properties.
The construction therefore solves two problems together: removing the extra constant and preparing the entries for denominator estimates.
This is a useful way to understand mathematical invention. A formula can be analytically attractive but arithmetically unusable. Changing how the same ingredients interact can reveal cancellation that a crude estimate would overlook. Here that cancellation is what lets the rationality assumption reach the entire determinant.
7. Denominator Control and the Nonvanishing Problem
For a nonzero rational number whose denominator divides an integer (D), its absolute value is at least (1/D). The manuscript develops a much more structured version of this principle by examining prime valuations, which record powers of primes in numerators and denominators.
The prime 2 receives separate treatment. At relevant large odd primes, the argument must control contributions corresponding to both (p^2) and (p). Cancellation at one layer does not automatically control the other.
There is another requirement: the determinant must actually be nonzero. Zero satisfies every smallness estimate and produces no contradiction.
Because the determinant is mixed and signed, the paper cannot simply borrow positivity from a positive-moment construction. Instead, at sufficiently large prime scales (N=p), it reduces the problem to three fixed rational matrices.
An exact certificate checks their invertibility modulo 101. Their denominators are valid for reduction modulo that prime, and the listed elimination pivots are nonzero. This establishes nonvanishing over the rationals for the fixed matrices.
The reduction then provides an unbounded sequence of nonzero growing determinants under the rationality assumption. The modulus 101 certifies the fixed calculation. It is distinct from the varying primes used to generate that sequence.
8. The Analytic Bound and the Final Contradiction
On the analytic side, the paper expresses the determinant through integrals and controls the resulting evaluations. One estimate uses holomorphic interpolation, while a Hadamard bound handles complementary configurations.
Uniformity is essential. Integration points can approach one another, so an estimate that breaks down near collisions would leave part of the integration domain uncontrolled. The paper’s interpolation argument avoids introducing an uncontrolled inverse-Vandermonde factor.
The remaining products lead to logarithmic interactions. Chebyshev expansions, endpoint estimates, and explicitly chosen rational coefficients reduce the task to certifying bounds for certain functions.
The final comparison uses the normalized quantity
[ L_N=\frac{\log|\Delta_N|}{(48N)^2}-\frac12\log2. ]
Under rationality, the arithmetic argument gives
[ \liminf L_N>-2.29084 ]
along the nonzero prime-scale sequence. The analytic argument gives
[ \limsup L_N\leq-2.290939875. ]
The second number is smaller than the first. No sequence can satisfy those two restrictions, so the rationality assumption fails.
The normalization is important for interpretation. These decimals are bounds on a logarithmic growth rate, not estimates of (G) itself. Their small separation becomes decisive because the underlying logarithm scales with the square of the matrix size. A narrow but rigorous asymptotic advantage is enough to force incompatibility.
The narrow gap explains the care devoted to certificates. Locating plausible maxima numerically would not establish a global upper bound. The manuscript instead certifies stationary points and bounds intervals containing them. Exploration can suggest the winning parameters, but rigorous inequalities have to finish the proof.
9. What Lean Verification Covers
OpenAI’s documentation for family 005 states that the formalization proves irrationality of the explicit series defining (G). That scope matches the headline theorem, rather than a weaker nearby statement.
A Lean proof is different from asking a language model whether a manuscript looks correct. The formal derivation is checked against rules and definitions by a proof checker. That can provide strong evidence of logical correctness within the chosen foundations.
Readers may nevertheless encounter sorry in the comparator file. In Lean, sorry supplies an unfinished proof. In this repository, that file presents the target assertion against which a separate proof implementation is compared. Its placeholder is not evidence that the separate implementation necessarily contains the same gap.
A meaningful independent audit follows the whole route: reproduce the relevant checks, inspect the exact statement, examine its definitions and assumptions, and confirm that the implementation proves the intended assertion without unintended additional axioms.
This article does not report an independently reproduced build. The documentation’s claim and that additional verification step should remain distinct.
Formal checking also cannot explain why the construction was discovered, whether every optimization is illuminating, or how broadly the method generalizes. A proof can be correct and still need substantial exposition. For researchers, understanding its reusable ideas is part of the value.
That is why a readable account matters alongside formal verification. It lets another mathematician see which hypotheses do the work, where estimates are tight, and which choices might be changed. Reusability often begins with explaining the purpose of a lemma that otherwise looks like an isolated technical hurdle.
10. Why the Earlier Sun Proof Is a Separate Case
Zhi-Wei Sun’s September 3 preprint claimed the same qualitative result. Dane Wachs’s September 16 critique examined its derivation through exact computations and arithmetic identities.
The critique identified an unjustified estimate in the final asymptotic accounting. In particular, the contribution from the prime 2 was not adequately carried through the argument intended to establish smallness. Wachs concluded that the published derivation did not justify the crucial estimate, leaving the main proof incomplete.
That conclusion does not establish rationality. An unsuccessful irrationality argument tells us about the argument, not the opposite truth of its target.
It also does not refute OpenAI’s later paper. The manuscript cites Sun’s preprint but explicitly states that no result from it is used. Citation and theorem dependence are different relationships. Claims about broader inspiration would require further evidence.
11. What Changes and What Remains Unresolved
The manuscript gives geometric consequences as well. With sectional curvature normalized to (-1), Agol’s theorem identifies (4G) as the minimum volume of an orientable, complete, finite-volume hyperbolic three-manifold with exactly two cusps.
Irrationality of (G) makes that volume irrational. The paper also derives irrationality for certain arithmetic hyperbolic volumes that are positive rational multiples of (G).
But is Catalan’s constant transcendental? This argument does not answer that question. Transcendence excludes roots of every nonzero integer polynomial. Irrationality excludes only ratios of integers. The familiar number (\sqrt2) illustrates the difference: it is irrational but satisfies (x^2-2=0).
The manuscript also does not provide an irrationality measure, which would quantify restrictions on rational approximation. Its qualitative contradiction supplies less information than such a quantitative theorem.
Whether these determinant constructions can resolve other special-value problems remains a question for further work. The method offers a direction to investigate, not an automatic general-purpose solution.
12. Why This Argument Is Worth Understanding
The lasting interest in Catalan’s constant irrationality is the obstacle the manuscript claims to overcome. Fast approximation had not been enough. The new construction coordinates cancellation, denominator estimates, nonvanishing, and certified analytic bounds until rationality leaves no room for the resulting sequence.
For AI readers, that is the meaningful development: a proposed research contribution whose mathematical mechanism can be examined, checked, and potentially reused. For researchers and builders, the useful next step is to distinguish the verified assertion from the methods still requiring explanation and broader investigation.
Follow Binary Verse AI at binaryverseai.com for research explainers that trace the original problem, the new argument, and the evidence behind the headline. The point is to understand what a breakthrough actually changes.
1. What is Catalan’s constant, and what is its value?
Catalan’s constant is the number
\[ G=\sum_{n=0}^{\infty}\frac{(-1)^n}{(2n+1)^2} =1-\frac19+\frac1{25}-\frac1{49}+\cdots \approx0.915965594177219. \]
It is also the Dirichlet beta function’s value at \(2\), written \(\beta(2)\). Catalan’s constant is distinct from Catalan numbers and Catalan’s conjecture.
2. Is Catalan’s constant irrational, and what has Lean verified?
OpenAI’s manuscript dated September 24, 2026, claims a proof that Catalan’s constant cannot be expressed as a ratio of integers. Its accompanying documentation states that the Lean formalization proves the irrationality of the defining series. Independently reproducing and auditing that formal proof is a separate verification step. A sorry in a comparator target file does
3. Why was Catalan’s constant so difficult to prove irrational?
Finding fractions close to Catalan’s constant was not enough: their denominators could grow too quickly. Earlier constructions needed the nonzero quantities \(q_nG-p_n\) to approach zero after denominator clearing, and their estimates did not achieve that. OpenAI’s manuscript instead compares arithmetic lower bounds and analytic upper bounds for specially constructed determinants.
4. Wasn’t a proof of Catalan’s constant irrationality already found to contain errors?
The September controversy concerned Zhi-Wei Sun’s separate manuscript. Dane Wachs’s critique concluded that its published derivation did not justify a crucial estimate, leaving the proof incomplete. That does not show Catalan’s constant is rational or refute OpenAI’s later manuscript, which explicitly states that it uses no result from Sun’s preprint.
5. Does irrationality prove that Catalan’s constant is transcendental?
No. Irrationality means a number cannot be written as a ratio of integers. Transcendence means it satisfies no nonzero polynomial equation with integer coefficients, which is a stronger property. OpenAI’s manuscript proves qualitative irrationality; it does not establish transcendence or provide an irrationality measure for Catalan’s constant.