Formalization in Lean 4

Let $N \ge 10$ be an even number that admits an off-diagonal Goldbach pair — a pair of primes with $p + q = N$ and $p \ne q$. Then the indicator $F_N$ is not a coboundary on primes.

The formal definitions of the indicator $F_N$ and of the notion of a coboundary are given in the file itself; the present page gives only the informal reading. The proof is complete — the file contains not a single sorry.

These files turn Theorem JP1 into an explicitly checkable fact for an initial range: the decide tactic mechanically enumerates and certifies the statement for all even $N$ from 10 to 1000.

A decide certificate is not a numerical experiment but a fully fledged proof built by computation inside the logic: the kernel checks each case, and no assumptions are involved. Hence the word unconditional in the file name.

The PMAP core contains exact rational exponent identities and congruence equivalences on which the subsequent constructions of the project rely.

The core is deliberately written without Mathlib: it is self-contained and does not pull in the external library. It contains no sorry and no axiom commands, and it sits under the CI ban of check_lean_core — a regression here cannot pass unnoticed.

The PPE chain — the attempted route from Möbius cancellation to the conjecture — is refuted in Lean: the file constructs an explicit counterexample in which cancellation is present only over composite numbers and proves that this does not suffice to derive the conjecture. The refutation itself is a theorem: the counterexample is checked by the kernel in full.

The inequality is proved in Lean as an exact statement. For orientation: the left-hand side is approximately 0.7506, which indeed exceeds 0.7.

The family of files LiLiu*.lean checks finite constants and budgets of the sources — the accounting of how the contributions of individual estimates fit into the overall balance of the corresponding works.

These checks do not re-prove the works themselves in full: they certify only the finite numerical statements on which those works stand.

Formal bookkeeping for the currently active line of work — a source-level replay of the Huang–Li conditional route. Lean proves the internal reductions: that the full $\mathrm{EH}_\mu$ hypothesis implies its fixed-class form; the transfer from the unweighted fixed-class estimate to its log-weighted form; a pure level-arithmetic combination of the stated inputs; and the finite endpoint and coprimality repairs used in the replay. The analytic hypotheses themselves enter only as explicit statement objects — definitions, with no sorry and no axiom in these two files — and remain open: no new estimate is proved here, and this work does not change the status of the conjecture.

Full lake build GoldbachFormalization passes against the pinned Mathlib revision are on record in the project’s pass ledger (most recently in the July 2026 passes). A successful build, however, is not a claim of completeness: Lean happily compiles modules that contain sorry scaffolds and axiom declarations, so a green build certifies only that what is proved type-checks. The complete inventory of the remaining gaps is itemized below, and the Mathlib-free PMAP core additionally passes the stricter check_lean_core audit.

As of the 2026-07-19 snapshot the formalization contains exactly one sorry — in GoldbachPairTactic.lean (line 40): the correctness theorem for the search function findGoldbachPair, whose proof would require an induction over the function’s well-founded recursion. The lemma is off the critical path: no downstream result depends on it — the concrete Goldbach-pair instances used elsewhere are proved directly by decide, bypassing the function, and sample evaluations of the function itself are checked with native_decide. It is counted here as an open gap and nothing else.

Every axiom declaration in the formalization layer, by file:

An axiom here is an honest marker: “this input is assumed, not proved”. Introducing axioms for open bridge statements is forbidden by the project’s guardrails; the declarations above record classical results, external sources, or explicitly open hard inputs.

An earlier version of this file carried a sorry for a sieve argument that, on audit, did not prove what it was meant to prove: the nearest audited theorem in the literature is substantially weaker than the claim the scaffold assumed. The unsupported sorry has been removed; the file now only defines the target as an explicitly unproved proposition — nothing is proved in SmallChen.lean itself, and the accompanying finite arithmetic repair is proved in PPEChain.lean. The line of argument it served has been refuted — see the parity barrier page. The file is kept deliberately, as a documented dead end: erasing the traces of failed approaches is poor research practice.

The root of the repository contains BLUEPRINT.md, a complete map of every sorry in the project together with an effort estimate for closing it. Anyone may compare the statements made on this page with the actual state of the code.