What happened?
Captain Sude publicly attributed to GPT-6 Astra an unconditional proof that every even integer N > 2 can be written as N = a + b with positive integers a and b satisfying lambda(a) = lambda(b) = -1. The released paper and Lean theorem state this all-even result without GRH or a sufficiently-large restriction. This is a Liouville analogue of binary Goldbach, not a proof of the classical Goldbach conjecture.
The public project supplies an authorless mathematical paper, a complete Lean 4 formalization against mathlib's Liouville function, pinned toolchain metadata, build and axiom audits, and proof-route checks. A separate audit repository independently rebuilt the frozen v1.0.0 artifact on Linux, matched the source hashes, repeated the axiom and route audits, and reported no sorry, custom theorem axiom, or native_decide. The public paper and repository do not preserve a detailed model–human derivation trace, so the precise division of intellectual labor remains source-attributed rather than independently reconstructed by the Chronicle.
Why it matters
Mangerel's 2024 Shusterman paper obtained the same (-1,-1) sign-pattern conclusion only under GRH and for sufficiently large even N. The new release claims to remove both restrictions and packages the argument as a reproducible formal artifact. If the mathematical novelty and reported Astra provenance continue to withstand specialist scrutiny, it is evidence of AI participation in resolving a concrete open research problem rather than merely improving a benchmark.
Significance rationale: The release addresses a named open Liouville–Goldbach problem by giving an unconditional all-even theorem where the closest direct predecessor required GRH and sufficiently large even inputs. The result is accompanied by a complete Lean formalization and an independent technical replay, making it a substantive AI-associated research milestone while remaining distinct from the classical binary Goldbach conjecture and below the Chronicle's H1 historical threshold.
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Partially verified
- Evidence level
- E4 · Independent check
- AI role
- Unclear
- Formal assurance
- Independently replayed
How should these labels be read? →
Contribution & verification
- Mathematical novelty
- New result
- Interface
- Informal, Formal, Symbolic, Hybrid
- AI contribution
- Captain Sude publicly attributes the proof discovery to GPT-6 Astra, including a first multiples-of-four argument followed by a new route covering every even integer greater than two. The released paper and repository do not document enough interaction provenance to independently separate model-generated ideas from human problem selection, prompting, editing, proof repair, or formalization work.
- Human contribution
- Captain Sude maintained and released the public project materials and publicly described the Astra attribution. The released record does not document the exact human contribution to target selection, prompting, manuscript editing, Lean proof repair, or verification, so those roles are not inferred more specifically here.
- Verification
- Partially verified · E4 · Independent check · Independently replayed
- Last reviewed
- 2026-09-27
Technical details
- Systems
- gpt-6-astra, lean
- Organizations
- —
- Problems
- liouville-goldbach-problem
- Methods
- multiplicative-functions, finite-field-symmetry, descent, quadratic-reciprocity, formalization
Verification history
- 2026-09-16 · Paper released · E3 · Inspectable artifact
The public repository released the mathematical paper and a complete Lean formalization whose final theorem matches the stated all-even Liouville–Goldbach claim. The project records successful local build, axiom, and proof-route audits.
- 2026-09-17 · Partially verified · E4 · Independent check
An independent audit repository reports a Linux rebuild of the frozen v1.0.0 release, zero source-hash mismatches, a fresh axiom audit, a successful route audit, and no sorry, custom theorem axiom, or native_decide. This supports independently_replayed formal assurance but is explicitly a technical reproduction rather than independent mathematical peer review or priority adjudication.
Corrections
No corrections recorded.
