Haglund's Zero-Trajectory Conjecture for the First Riemann Xi Approximant

Haglund's Conjecture 4 reads: for $k\ge1$ , the imaginary part of each non-real zero of $\Xi_k(z)+t\Phi_{k+1}(z)$ decreases monotonically as $t$ goes from 0 to 1, where the $\Phi_n$ are the incomplete-gamma summands of Riemann's series for $\Xi$ and $\Xi_k=\sum_{n\le k}\Phi_n$ . This work proves the case $k=1$ , the pencil $\Phi_1+t\Phi_2$ : every non-real zero in the closed first quadrant is simple and the imaginary part of its analytic branch strictly decreases. It adds two statements Conjecture 4 does not itself assert - no non-real branch escapes to infinity on a bounded forward parameter interval, and at a real collision of any finite multiplicity the full local Weierstrass-Puiseux multiset stays real to the right. The cases $k\ge2$ remain open, and nothing is claimed about the zeros of $\Xi$ or the Riemann hypothesis.

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Computation
Field: Analytic number theory and entire-function zero dynamics
Posed by: James Haglund
Year posed: 2009
Years open: 17y
Solved: 2026-08-22
Model: ChatGPT and Codex
Vendor: OpenAI
Collaborators: —
Verification: Site-confirmed
Publication: Preprint
Significance: 8 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Proves Haglund's Conjecture 4 for $k=1$ : every non-real first-quadrant zero of $\Phi_1+t\Phi_2$ is simple with strictly decreasing imaginary part, no branch escapes forward, and every finite-multiplicity real collision stays real afterwards. The cases $k\ge2$ remain open. Two readings worth separating: Conjecture 4 asserts the monotone descent alone, so the no-escape and stays-real statements are this paper's own additions rather than Haglund's text, and they are the stronger part of the theorem. The descent itself, part (i), is the part that rests on the unavailable interval-arithmetic certificate.

What the AI did

The disclosure was rewritten on 25 August, and now reads in full: "OpenAI ChatGPT and Codex models performed most of the proof search, mathematical derivation, computational implementation, Lean proof development, literature discovery, organization, and drafting. The author supplied the research methodology, problem framing, constraints, evaluation criteria, and iterative oversight. The author remains responsible for every mathematical statement, proof, citation, and submission decision." That names the systems and attributes the proof search itself to them, which is why this is filed as AI-discovered. It replaces the earlier version - "AI systems were used extensively in mathematical derivation, Lean proof development, literature discovery, organization, and typesetting" - which named no system and attributed no step, and on which this entry was first filed a rung lower as co-developed. The manuscript still gives no version for either system, so the model field records only what it says.

Verification

Site-confirmed: the computational certificate was replayed here on 26 August 2026 and it passes. Cloned mbaccaro-dev/mathematical-proofs, installed python-flint 0.9.0 into a venv per requirements.txt, ran its own reproduce.py in full (4 min 17 s), and got STATUS=PASS with claim_ceiling=Haglund_Conjecture_4_for_k_equals_1_only - via MANIFEST_PASS at 289 files, S1_STRUCTURE, NONREAL_JOIN, GLOBAL_LIFT, OUTER_REGION, and crucially S2_SCIENTIFIC_PASS at patches=238, source_calls=60930, the paper's own figures for the certified first-quadrant proposition, plus S3 at 323 patches and 46,514 calls.

What that does not settle: the script recomputes its own certificates against its own manifest, so it shows the computation replays and is internally consistent, not that the interval arithmetic implies the theorem (argued in prose) nor any analytic step around it. The Lean is unchanged from first review - no sorry, admit or declared axiom in the Solution closure, but it verifies one abstract collision theorem, and the repository still says the atlas, the incomplete-gamma estimates and the assembly are not consequences of it. End-to-end Lean remains pending by the author's account; the paper is unrefereed.

One packaging defect found while replaying: on a fresh clone reproduce.py aborts at the manifest gate. Of 289 hashes, 12 match only as CRLF, all Windows console receipts, and with no .gitattributes no checkout satisfies both sets; the run above needed those 12 converted first.

Sources

Submitted by WildHeron785 on 24 Aug 2026

Rasmus Lindahl26 Aug 2026, 12:07 UTC

Replayed it here, and it passes. Thank you for publishing the archive.

What I ran, on 26 August: cloned the repository, installed python-flint 0.9.0 into a venv per requirements.txt, and ran reproduce.py in full. Four minutes seventeen seconds, ending

STATUS=PASS claim_ceiling=Haglund_Conjecture_4_for_k_equals_1_only

with MANIFEST_PASS at 289 files, then S1_STRUCTURE, NONREAL_JOIN, GLOBAL_LIFT and OUTER_REGION, and the two atlases at S2 patches=238 source_calls=60930 and S3 patches=323 source_calls=46514. The S2 line reproduces the paper's own figures for the certified first-quadrant proposition, which is exactly what the claim-issue flag said no reader could replay. The flag is removed and verification moves to site-confirmed, with the note recording precisely what was run.

Two other things followed from your update. Your rewritten disclosure now names the systems and says they "performed most of the proof search", so AI contribution goes back up to AI-discovered - I said at review that naming the system and its role would move the tier the same day, and it does. The model field now reads "ChatGPT and Codex", matching the paper rather than a version it never states.

One defect worth fixing, because it stops the next reader cold. On a fresh clone reproduce.py aborts at the manifest gate. Of the 289 hashes, 277 match a LF checkout and 12 match only as CRLF - all Windows console receipts (source_stdout_*, source_watchdog_*). There is no .gitattributes, so no single checkout satisfies both sets: autocrlf=true breaks the .py files, autocrlf=false breaks those 12. I converted exactly those 12 locally and the run then completed. A .gitattributes pinning them, or regenerating the manifest from normalised bytes, would make it clone-and-run.

Resolution stays candidate, and that is not a comment on the computation. The analytic half still has no independent review, and end-to-end Lean is pending by your own account.

Haglund's Zero-Trajectory Conjecture for the First Riemann Xi Approximant

What was actually shown

What the AI did

Verification

Sources

Discussion2