Source and verification

This article explains family 005 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ Catalan’s constant and rational approximation

Catalan’s constant is

The series converges absolutely. It is the value of the Dirichlet beta function . The manuscript in this family claims that is irrational. It does not claim an upper bound for its irrationality exponent. (OpenAI, 2026)

A useful integral is

Indeed, on , the Taylor series of is . Its integrated absolute term masses sum to , justifying termwise integration on .

This represents the constant by a smooth moment integral, but it does not settle irrationality. Many rational numbers also have integral representations and rapidly convergent rational approximations.

🏷️ The arithmetic obstruction

Suppose a real number is rational. For integers , a nonzero linear form satisfies

Thus nonzero integer linear forms tending to zero prove irrationality. A small rational linear form does not suffice: its denominator may grow faster than its numerator shrinks.

The source uses a higher-dimensional version of this principle. It constructs signed moment determinants of size . Under the assumption , their entries and determinants are rational. Prime-by-prime denominator estimates provide a lower bound on the absolute value of a nonzero determinant, while an integral formula provides an incompatible upper bound.

The proof therefore has three distinct obligations: rationality under the hypothesis, nonvanishing on an unbounded sequence, and a strict separation of the two size estimates. Neither a small determinant nor formal cancellation establishes all three.

🏷️ Moments, cancellation, and nonvanishing

The initial moments involve rational combinations of , , and . Here . Carefully selected polynomial rows cancel the coefficient in every matrix entry. Entrywise cancellation is essential: assuming rational should make the entire matrix rational before any determinant estimate is applied.

The rows also have high Taylor contact and divisibility properties. Contact of order means that the first Taylor coefficients of the relevant difference vanish. It creates analytic smallness, while integral polynomial coefficients allow arithmetic divisibility to be counted.

Because the determinants are signed, their integral representations are not positive measures whose nonvanishing follows automatically. The source instead takes along large primes, uses reduction modulo , and changes between two bases. The growing-dimensional rank problem reduces to three fixed rational matrices. An exact finite certificate is then used to establish nonvanishing along an unbounded subsequence. This note has not executed that certificate.

For comparison, a positive Gram determinant has the form and is positive for independent vectors. The source’s mixed moment determinant has no such immediate positivity justification.

🏷️ The analytic determinant estimate

An integration identity of Andréief type converts a determinant of integrals into an integral of a product of evaluation determinants. This permits the logarithm of its size to be compared with an interaction energy of the integration variables. Chebyshev expansions organize that energy into tractable terms.

Two issues prevent a direct application of a pointwise estimate. First, the rational parametrization has two branches, both of which must contribute to a valid upper bound. Second, nodes can coalesce. Inverting an evaluation matrix would introduce a potentially large inverse Vandermonde factor near collisions. The source instead cancels that determinant algebraically in a finite Hardy-space operator formulation.

A bounded holomorphic interpolant treats one range of configurations; a Hadamard determinant bound treats the complement. The logarithmic interaction is regularized before diagonal and endpoint limits are taken. Finally, a rational trial certificate bounds the resulting one-variable optimization on complete intervals containing all stationary points, rather than evaluating a numerical grid. These are the main analytic mechanisms described in the manuscript. (OpenAI, 2026)

🏷️ The contradiction at quadratic scale

Write

Under the rationality assumption, the source obtains, along its nonzero subsequence,

Its analytic estimate gives

The intervals are disjoint. That strict gap, together with nonvanishing and denominator control, is the claimed irrationality argument. The printed decimals express certified bounds in the source; they are not numerical observations from approximating .

The ordinary prime number theorem enters the arithmetic estimate. The paper also derives geometric consequences, but the central graduate-level lesson is the separation between real smallness, arithmetic discreteness, and determinant rank.

🏷️ Key steps and proof outlines

The following outlines unpack the source’s sections “Polynomial rows and mixed moments,” “Odd primes and the finite-place lower bound,” “Nonvanishing along the prime sequence,” and “The real-place determinant estimates.” The arithmetic and analytic estimates apply to the same determinant. Changing the rows to improve one estimate would require rechecking the other. (OpenAI, 2026)

Entrywise cancellation by Taylor contact

Put and write for the coefficient of in a power series . The source constructs integer polynomials , indexed by , satisfying

To specify the determinant, define the bilinear moment forms

Write and similarly for . With and , the determinant is

After integration in , the absolute kernel is bounded by a constant times , which is integrable at the endpoints. Polynomial factors are bounded, so these moments are well defined.

Taylor contact is a finite list of exact coefficient identities. The mixed moments and have rational parts and coefficients multiplying and . In their combination , the coefficient of is exactly

Proof outline. Expand , insert the moment evaluations, and collect the coefficient. The convolution of the coefficients of with those of is precisely the displayed coefficient extraction. Contact makes it zero for every raw column . The actual columns use ; expanding the last factor only uses raw columns with . Thus this integer column operation preserves cancellation. Every final entry lies in , so assuming rational makes the determinant rational. The point is to cancel the unwanted constant before estimating a determinant; cancellation of a few leading asymptotic terms would not establish rationality.

Arithmetic size from valuations

For a nonzero rational number , let be the exponent of in its numerator minus that in its denominator. Unique factorization gives the exact identity

Proof outline. The source groups the raw columns according to their residue indices at an odd prime and eliminates columns over the local integers, meaning that the operations introduce no denominator divisible by that prime. Dependencies between the leading residue layers improve the determinant valuation beyond the sum of crude entrywise bounds. After the integer column filter, these losses form a piecewise linear function of . Summing its pieces with the prime number theorem produces a bound of order . The prime has a separate argument: factorial valuations and a convergent -adic moment expansion give

Inserting all these lower bounds into the exact logarithmic identity yields the previously stated lower bound on . The error depending on the hypothetical rational value of disappears after division by . The nonzero condition is indispensable here: is not finite when the determinant vanishes.

Nonvanishing through a fixed-size block calculation

Take prime, outside the finitely many exceptional prime divisors of fixed denominators. Multiplication of every matrix entry by produces a matrix integral at . Its reduction modulo can be transformed into

where have size , , and for . A tensor product here simply means a block matrix: its block is the scalar entry of the first factor times the second factor.

Proof outline. Write each row index as and use the identity modulo to separate the scale- row into two scale-one rows. An invertible triangular change between two polynomial bases gives the displayed block form. Each pair has a symmetric and an antisymmetric vector, on which acts by and . Together with , these split the determinant into factors and . The source’s exact certificate shows these three fixed rational determinants are nonzero. They remain nonzero modulo every sufficiently large prime, so the scaled determinant is a unit at . Consequently

which proves nonvanishing along an unbounded sequence. This explains how a finite certificate can serve every large scale; it is not an extrapolation from numerical determinants of increasing size.

From a determinant to an interaction energy

When all the products in the determinant expansions are absolutely integrable, Andréief’s identity is

Proof outline. Expand both determinants on the right as signed permutation sums, use Fubini, and relabel the integration variables. Each permutation produces the same determinant on the left, giving the factor . In this paper one applies the identity twice, because each entry is a double integral. The middle determinant is a Cauchy determinant:

Taking logarithms of the absolute integrand turns products over pairs into a logarithmic energy of order . The remaining evaluation determinant contains both branches of the parametrization. The source bounds it by combining bounded holomorphic interpolation with Hadamard’s inequality; its operator formulation cancels a Vandermonde factor before nodes collide. The energy estimate uses the elementary inequality , obtained from , with freely chosen trial coefficients . Applied to the negative quadratic Chebyshev-coefficient terms, it replaces interactions by affine terms and reduces the upper bound to two one-variable suprema. The certificate brackets every possible stationary point and controls the derivative between brackets, so its conclusion concerns entire intervals, not sampled points. Regularization permits passage to limiting configurations, and this certified energy bound yields . Comparing this with the arithmetic lower bound on the nonzero prime sequence finishes the claimed contradiction. These outlines explain the interfaces; the lengthy prime-layer estimates and certified energy optimization remain substantive parts of the manuscript.

🏷️ Connections

The irrationality exponent of pi uses another interpolation-determinant comparison. Its target is a sharp approximation exponent, whereas the present family establishes only the qualitative irrationality assertion.

🏷️ Manuscripts and verification scope

The family scope page describes selected formalization coverage. The selected statement is irrationality of Catalan’s constant; no approximation exponent is claimed. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. Catalan’s constant is irrational.