we-solve (beta)

Math-2218 · mathematics · Analysis

Flint Hills series

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Does the Flint Hills series $\sum_{n=1}^{\infty} 1/(n^3\sin^2 n)$ converge?

Formulation references: [S1], [S2].

Short English statement

Does the Flint Hills series $\sum_{n=1}^{\infty} 1/(n^3\sin^2 n)$ converge?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2218-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2218

The irrationality-exponent manuscript explicitly concludes convergence of the exact Flint Hills series displayed in this question, with angles in radians. Its ineffective threshold concerns the auxiliary approximation bound for $\pi$ and does not weaken the asserted convergence.

Flint Hills series

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 017; 2026-09-24), the asserted result is that the irrationality exponent of $\pi$ equals two, which also implies convergence of the classical Flint--Hills series.

Mathematical statement of the claimed result

Manuscript 1.
For every real $\nu>2$, the claimed integer threshold $Q(\nu)$ satisfies \[ |\pi-p/q|\ge q^{-\nu}\qquad(p\in\mathbb Z,\ q\ge Q(\nu)). \] Thus the irrationality exponent of $\pi$ is two. The threshold is not claimed effective, and this does not assert a fixed positive lower bound $c/q^2$. The cited direct consequence is \[ \sum_{n=1}^{\infty}\frac1{n^3\sin^2 n}<\infty, \] with angles in radians.

Outline of the argument

For manuscript 1 (family 017; 2026-09-24), an interpolation determinant uses separated coordinate weights that remain valid independently of the chosen points. A full-rank minor has a lower arithmetic size, while repeated Taylor degrees give a quadratic analytic saving; a local multiplicity comparison turns the contradiction into the optimal approximation exponent.

Formal verification

For manuscript 1 (family 017; 2026-09-24), the documented Lean scope is the approximation exponent of $\pi$, including its exact value two; the Flint--Hills-series consequence is absent from the selected statement.

This coverage does not establish a formal proof of the complete problem as stated here.

The linked family Comparator checks are PiExponent.lean.

Their named declarations include OAI.PiExponent.main.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →