VibeMathedMath problems solved with AI
Sign in

Goldbach's conjecture for the Liouville function

The Liouville function λ(n)\lambda(n) is +1+1 or −1-1 according to the parity of the number of prime factors of nn counted with multiplicity. In August 2018 a MathOverflow question asked for a Goldbach-style statement about its sign: is it true that for every even integer N>2N > 2 there are positive integers a,ba, b with a+b=Na + b = N and λ(a)=λ(b)=−1\lambda(a) = \lambda(b) = -1? The case N=2N = 2 fails. Sieve methods run into the parity obstruction here, so the question resisted the obvious attacks.

Result
Proved(see note)
Status
Resolved
AI contribution
AI-discovered
Method
Argument
Field
Multiplicative number theory
Posed by
Asked by the MathOverflow user Pablo, question 307479, 3 August 2018; attributed in the Lean development to a formulation of Shusterman
Year posed
2018
Years open
8y
Solved
2026-09-16
Model
ChatGPT-6 Astra
Vendor
OpenAI
Collaborators
—
Verification
Lean-verified
Publication
Announced
Significance
22 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

True: for every even N>2N > 2 there are positive a,ba, b with a+b=Na + b = N and λ(a)=λ(b)=−1\lambda(a) = \lambda(b) = -1, unconditionally, with no analytic or conjectural hypothesis. The route reduces to a prime modulus, then uses λ(2n)=λ(3n)=λ(5n)=−λ(n)\lambda(2n) = \lambda(3n) = \lambda(5n) = -\lambda(n) to force λ\lambda to agree with the Legendre symbol on an interval, where quadratic reciprocity gives a contradiction; no sieve is used, which is how the parity obstruction is avoided.

Two pieces of context a reader needs. Mangerel (IMRN 2024) proved that λ(a)λ(N−a)\lambda(a)\lambda(N-a) cannot be constant for N≥11N \ge 11; that yields a pair with opposite signs and so does NOT imply this statement. And the result has since been generalised: on the same MathOverflow question, Lingsen Meng gives an unconditional argument that all four sign pairs occur for every N∉{2,3,4,5,6,9,10}N \notin \{2,3,4,5,6,9,10\}, covering odd NN too, while crediting this work as independent and prior for the even case.

What the AI did

The AI chose the problem, proved it and then formalized the result in Lean.

Verification

Audited here on 30 September 2026 from a clone at HEAD. Twelve Lean files, 1,689 lines on Lean 4.34.0-rc2: zero sorry, zero axiom declarations, zero native_decide. Audit.lean prints the axioms of liouville_goldbach and of twelve supporting results. GitHub Actions ran the Lean verification workflow green twice on 16 September, including at tag v1.0.0. Statement fidelity checked by hand against the MathOverflow wording: the headline theorem is liouville_goldbach (N) (hEven : Even N) (hN : 2 < N) concluding the existence of a, b with 0 < a, 0 < b, a + b = N and liouville a = liouville b = -1, which is the question exactly, with no extra hypothesis and nothing conjectural assumed. Independent corroboration, which is the other half of lean-verified: an answer posted to the same MathOverflow question on 25 September 2026 by Lingsen Meng states that for the even case an unconditional proof was given independently in September 2026 by an anonymous author together with a Lean formalization, and links this repository at release v1.0.0.

Sources

Submitted by nufrogcaca on

Changelog2 changes

Discussion