GPT-6 Astra solves a Goldbach-type conjecture with formal Lean proof

Mathematicians might be the single group of people with the lowest tolerance for AI hallucinations. A single misplaced minus sign can bring down months of work. But feed that reasoning directly into a rigid interactive proof assistant, and the game completely changes.

Independent researcher Captain Sude published a new repository on GitHub, announcing that GPT-6 Astra had solved a Goldbach-type conjecture regarding the Liouville function. Even better, the entire mathematical proof was formalized in Lean 4 and verified with zero gaps.

Breaking down evens into odd prime factors

Most people know the classical Goldbach conjecture: every even integer greater than 2 is the sum of two primes. A prime has exactly one prime factor, which is trivially an odd count.

The conjecture Astra tackled is a close cousin. In number theory, the Liouville function assigns a value of -1 to any integer with an odd number of prime factors (counted with multiplicity), and 1 if the count is even. The theorem states that every even integer N > 2 can be written as the sum of two positive integers a and b such that both have a Liouville value of -1.

The question was first posed on MathOverflow by user Pablo in August 2018, and later attributed by mathematician Mangerel to Shusterman. Earlier research provided key building blocks, including Bloom's scaling observation and Mangerel's arguments on rigidity and commuting defects.

Astra managed to construct an elementary proof. It pieced the solution together using two commuting symmetries, a descent argument, and quadratic reciprocity.

Passing the ultimate audit in Lean 4

To ensure no AI shortcuts or hand-waving slipped through, the author formalized the full proof using Lean 4.34.0-rc2 and mathlib.

The build logs, axiom audits, and proof-route checks all passed cleanly. The formal declaration relies solely on Lean's core logic foundations: propext, Classical.choice, and Quot.sound.

There are no hidden mathematical assumptions and no unfinished proofs marked with "sorry". Every commit on GitHub triggers fresh verification runs via Actions to keep the proof completely watertight.

Why it matters

We think this project demonstrates the gold standard for AI in scientific research: pairing frontier LLM reasoning with automated proof assistants.

Historically, when an AI claimed a mathematical breakthrough, human experts had to spend weeks untangling potential hallucinations. Lean eliminates that bottleneck entirely. If the compiler accepts the proof without extra axioms, the theorem is settled fact.

For mathematicians and developers, this setup is evolving from an interesting curiosity into an indispensable research assistant. Astra didn't just guess; it found an elementary bridge across disparate number-theoretic ideas.

For the AI landscape, it shows where the real frontier of high-end reasoning models lies. Moving beyond conversational fluff to rigorous formal math proves that long-chain reasoning is getting strong enough to crack problems that sat open in academic forums for years.