Results
What this project has obtained, and the precise status of every statement.
The main point first
The binary Goldbach conjecture — the assertion that every even integer greater than two is a sum of two primes — remains an open problem. This site does not prove it, and no result below comes anywhere close to a full proof. Nothing on this page should be read as “the conjecture is almost proved”.
At the same time, the project has produced concrete, honestly labelled outcomes: corollaries of published work by other authors, two conditional results, machine-checked certificates of finite computations, and one small unconditional theorem of a combinatorial nature. Every statement carries a status marker:
How to read this page. The marker indicates the epistemic status of the statement: what is proved unconditionally, what is derived from the work of others, and what holds only under an unproved assumption. The formulations are given verbatim, with all caveats — the caveats are part of the result, not a footnote.
Proposition (1+1.8)
Corollary of sourcesThe classical apparatus of sieve methods and weighted sums compares an even not directly with a sum of two primes, but with the weaker representation , where are prime and the second factor is controllably small: or prime with . Write for the weighted count of such representations. Three source papers then imply:
Proposition (1+1.8). For every sufficiently large even :
where counts weighted representations with or prime , and is the standard factor of the source papers.
Sources
- Runbo Li, arXiv:2405.05727 (version v4);
- Li–Liu, arXiv:2606.05224 (version v1, preprint, unreviewed);
- J. Wu, arXiv:0709.3764.
The machine-checkable part of the computation is isolated in the Lean module RunboLi180.lean, which certifies the key arithmetic:
Caveats.
- This is not the binary Goldbach conjecture: the representation admits a composite part with a small prime factor.
- It is a corollary of the work of others; no novelty or priority is claimed.
- The numerical integrals of the sources have not been independently interval-certified.
The exponent ladder
Corollary of sourcesThe same set of sources yields a whole “ladder” of exponents in the bound : the weaker the exponent required, the larger the constant that can be guaranteed. Every row is a corollary of the cited sources; none is a new theorem.
| Exponent | Guaranteed lower bound | Origin |
|---|---|---|
| result of the source | Li–Liu, preprint arXiv:2606.05224 (unreviewed) | |
| corollary of the sources | ||
| corollary of the sources; finite arithmetic checked in Lean | ||
| corollary of the sources — the proposition above |
Read top to bottom: the exponent weakens while the constant in front of grows. Each row is source-derived: a deduction from the cited works, not an independent result of this project.
Conditional theorem BK+
Conditional resultExceptional (Siegel) zeros of -functions are the principal theoretical obstruction to understanding the distribution of primes in arithmetic progressions. Here the logic is reversed: if an exceptional zero were to exist, Goldbach representations could be extracted from it.
Theorem BK+ (conditional). If there exists a real exceptional Dirichlet character for which has a real zero
with (the Goldfeld–Gross–Zagier constant), then — as stated in the draft — there is a constant such that for every even
where is the number of Goldbach representations of the even integer .
Caveats.
- The result is taken from an unpublished draft (the PDF is posted on the Publications page); it is unreviewed and has not been confirmed by independent sources.
- It is a conditional result: the existence of such exceptional zeros is not known and is considered unlikely.
- Status correction (May 2026). A source audit of the draft’s derivation found that it rests on an additional unproved input — a broad Hardy–Littlewood-type dominance assumption that has not been matched to any published theorem. The statement is therefore conditional on both the exceptional zero and that dominance input, which is strictly more than the Siegel-zero hypothesis alone. The machine-checked version in the project’s Lean layer records this input explicitly; the draft’s effectivity claim for the threshold constant was likewise downgraded — it is carried as a statement-only target, not a certified bound. Earlier wording on this site presented the theorem as conditional on the zero only, and was too strong.Relation to prior work. “Siegel zeros imply strong additive results” is an established genre: the archetype is Heath-Brown’s theorem (1983) that Siegel zeros imply infinitely many twin primes, developed further in the Friedlander–Iwaniec exceptional-character program. What the draft claims beyond that genre is an explicit, effective threshold for the binary Goldbach problem specifically; the comparison to the prior literature has not been independently reviewed.
Theorem JP1
TheoremA small but unconditional result of a combinatorial nature about the “Goldbach indicator” — the function encoding the Goldbach pairs of an even .
Theorem JP1. For an even having at least one off-diagonal Goldbach pair (a pair of distinct primes with ), the Goldbach indicator is not a coboundary on primes.
In symbols, with
the theorem asserts that there is no with for all primes — the indicator is not a “coboundary” (a difference of a one-variable potential) on the primes.
In addition, every even from 10 to 1000 has a machine-verified instance (kernel-checked via the decide tactic; per-instance certificates, not a single quantified theorem).
The formalization and the machine checking are contained in the Lean project — see the Formalization page. By itself this statement does not advance the binary conjecture, but it records a structural property of the indicator that may be useful for further analysis.
Why so many caveats
Because honest labelling is the main principle of the project. A corollary of sources does not become a new theorem by silence; a conditional result does not become unconditional by ambition; an interval certificate does not replace an unproved hypothesis. Every badge and every “Caveats” block records exactly the strength the statement actually has.
Does any of this advance the binary conjecture itself? No. The results above concern relaxed representations , conditional consequences of zeros that are not known to exist, and auxiliary combinatorial properties. The conjecture remains open, and no proof of it is claimed here.