VibeMathedMath problems solved with AI
Sign in

The irrationality exponent of arctangents of nonzero rationals is 2

The irrationality exponent of an irrational xx is μ(x)=sup⁡{ν>0:0<∣x−p/q∣<q−ν\mu(x)=\sup\{\nu>0:0<|x-p/q|<q^{-\nu} for infinitely many coprime integers p,qp,q, q≥2}q\ge2\}; Dirichlet gives μ(x)≥2\mu(x)\ge2 and almost every real has μ=2\mu=2. Upper bounds have been obtained for values arctan⁡(1/n)\arctan(1/n): Tomashevskaya (2008) gave a general estimate, Salikhov and Bashmakova (2020) improved the bounds for arctan⁡(1/3)\arctan(1/3) and arctan⁡(1/5)\arctan(1/5), and Bai (2026) reported μ(arctan⁡(1/2))≤8.585166…\mu(\arctan(1/2))\le 8.585166\ldots. Since arctan⁡1=π/4\arctan 1=\pi/4, the case r=1r=1 is the conjecture μ(π)=2\mu(\pi)=2. Is μ(arctan⁡r)=2\mu(\arctan r)=2 for every nonzero rational rr?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI co-developed
Method
Argument
Field
Diophantine Approximation
Posed by
—
Year posed
—
Years open
—
Solved
2026-10-12
Model
GPT-6 Astra
Vendor
OpenAI
Collaborators
Lily Zhang, Evan Li
Verification
Lean-checked, statement unaudited
Publication
Announced
Significance
60 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Claimed: for every nonzero rational rr, μ(arctan⁡r)=2\mu(\arctan r)=2, and for every rational r>0r>0, μ(r π)=2\mu(\sqrt r\,\pi)=2. Both are corollaries of a quadratic field criterion: if DD is a nonsquare integer, x≠0x\ne0 real, and e2Dx∈Q(D)e^{2\sqrt D x}\in\mathbb Q(\sqrt D) has norm one, then μ(x)=2\mu(x)=2, with an ineffective threshold. For D=−1D=-1 and x=arctan⁡rx=\arctan r, e2ix=(1+ir)/(1−ir)e^{2ix}=(1+ir)/(1-ir). The case r=1r=1 recovers the OpenAI release's μ(π)=2\mu(\pi)=2, already a Candidate here; the method adapts that manuscript's determinant argument with the interpolation theorems of Liu, Jiang and Zhang (arXiv 2610.10192, μ(log⁡r)=2\mu(\log r)=2).

What the AI did

The README and the preprint's AI declaration say GPT-6 Astra helped determine what follows from μ(π)=2\mu(\pi)=2 and the Liu-Jiang-Zhang interpolation theorems, and built the Lean repository, the authors being new to Lean. The authors say they derived the quadratic criterion independently themselves and checked the Lean statements.

Verification

No independent mathematician has checked this yet. Checked here on 3 November 2026 at commit e8c8406, the current head of main: the headline theorem arctanOfRationals in IrrationalityMeasureConstants.lean now states, for every rational r≠0r\ne0, irrationalityMeasure (Real.arctan r) = 2, with no hypotheses left over; QuadraticField.criterion discharges ExponentialCriterion, and the diff from 1bfa47b (read here on 15 October) changes only that hypothesis from r>0r>0 to r≠0r\ne0 and its nonvanishing step. irrationalityMeasure (StatementDefinitions.lean) is the supremum of real μ\mu with infinitely many rationals within 1/denμ1/\mathrm{den}^{\mu}, matching the posed definition for irrational xx. Grepped the project and its pinned dependency jdb19937/log-irrationality-measure (09aeeb0): no sorry, admit, axiom declarations, opaque, unsafe, native_decide or implemented_by. Not rebuilt here and the headline's axioms were not printed. The statement is the provers' own and not independently anchored (no Formal Conjectures or tracker statement; OpenAI's PiExponent comparator covers π\pi only), so the tier is Lean-checked. The preprint is unrefereed and calls itself preliminary.

Sources

Submitted by Pink on

Changelog2 changes

Discussion