Third-level log-concavity of the Riemann Xi kernel

TheoremDB P11158 · analytic number theory

Inferred from the community field; finer classification has not been reviewed.

Source catalogue assessmentAs of 2026-09-08Source & evidence ↓

Read original source ↗ 0 Submit progress Lean 4 ↓Discussion (0)

Problem statement

Let

\Phi(r)=\sum_{m\ge1}\pi m^2\bigl(2\pi m^2e^{4r}-3\bigr)e^{5r-\pi m^2e^{4r}},\qquad r\ge0,

be the classical Riemann $\Xi$ -kernel, with its usual even extension, and put $S_0(t)=\Phi(\sqrt t)$ for $t>0$ . Recursively define

S_{j+1}(t)=(S_j'(t))^2-S_j(t)S_j''(t).

It is known that $S_0>0$ and $(\log S_0)''<0$ , and Planat--Solé (2026) proved $(\log S_1)''<0$ ; hence $S_1,S_2>0$ . Determine whether

S_3(t)>0\qquad\text{for every }t>0.

Equivalently, prove that $S_2$ is strictly log-concave on $(0,\infty)$ , i.e. $(\log S_2(t))''<0$ for all $t>0$ , or disprove this by giving a rigorous point or interval on which $S_3\le0$ .

Lean 4

Not yet attached

No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.

Share a formalization →Verification guide ↗

Background

Additional formulation recorded by the source

With $S_0(t)=\Phi(\sqrt t)$ and $S_{j+1}=(S_j')^2-S_jS_j''$ , prove or disprove $S_3(t)>0$ for every $t>0$ .

Progress & source assessment

Source-reported assessment, retrieved 8 September 2026. Frontier Science has not independently reviewed this status.

Open. No signed Lean verification is attached to this problem or its selected resolution.

References

[1]TheoremDB P11158 link

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.