Skip to content

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:

TheoremConditional resultCorollary of sourcesConjectureOpen problem

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 sources

The classical apparatus of sieve methods and weighted sums compares an even N not directly with a sum of two primes, but with the weaker representation N=p+rq, where p,q are prime and the second factor r is controllably small: r=1 or r prime with rqa1. Write D1,a(N) for the weighted count of such representations. Three source papers then imply:

Proposition (1+1.8). For every sufficiently large even N:

D1,9/5(N)  >  320  C(N)Nlog2N

where D1,a(N) counts weighted representations N=p+rq with r=1 or prime rqa1, and C(N) is the standard factor of the source papers.

Sources

The machine-checkable part of the computation is isolated in the Lean module RunboLi180.lean, which certifies the key arithmetic:

4932625    32log54  >  710

Caveats.

  • This is not the binary Goldbach conjecture: the representation N=p+rq 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 sources

The same set of sources yields a whole “ladder” of exponents a in the bound D1,a(N)>constC(N)N/log2N: 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.

ExponentGuaranteed lower boundOrigin
(1+1.9)result of the sourceLi–Liu, preprint arXiv:2606.05224 (unreviewed)
(1+1.8995)0.0001C(N)Nlog2Ncorollary of the sources
(1+1.894)1400C(N)Nlog2Ncorollary of the sources; finite arithmetic checked in Lean
(1+1.8)320C(N)Nlog2Ncorollary of the sources — the proposition above

Read top to bottom: the exponent weakens while the constant in front of C(N)N/log2N grows. Each row is source-derived: a deduction from the cited works, not an independent result of this project.

Conditional theorem BK+

Conditional result

Exceptional (Siegel) zeros of L-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 χD(modD) for which L(s,χD) has a real zero

β1=1δ1,δ1    clog2D

with c4108 (the Goldfeld–Gross–Zagier constant), then — as stated in the draft — there is a constant C>0 such that for every even

N  >  N3(D)  :=  exp ⁣(C/δ1)one hasr(N)>0,

where r(N) is the number of Goldbach representations of the even integer N.

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 N3(D)=exp(C/δ1) for the binary Goldbach problem specifically; the comparison to the prior literature has not been independently reviewed.

Theorem JP1

Theorem

A small but unconditional result of a combinatorial nature about the “Goldbach indicator” FN — the function encoding the Goldbach pairs of an even N.

Theorem JP1. For an even N10 having at least one off-diagonal Goldbach pair (a pair of distinct primes pq with p+q=N), the Goldbach indicator FN is not a coboundary on primes.

In symbols, with

FN(p,q)={    1p,q prime,  p+q=N,  p<q,1p,q prime,  p+q=N,  p>q,    0otherwise,

the theorem asserts that there is no φ:NR with FN(p,q)=φ(p)φ(q) for all primes p,q — the indicator is not a “coboundary” (a difference of a one-variable potential) on the primes.

In addition, every even N 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 N=p+rq, 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.