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\mathrm{\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 of Theorem JP1 is complete — the file contains not a single sorry.

Five instance files (UnconditionalJP1, ExtendedJP1, ExtendedJP1_500, ExtendedJP1_1000, ExtendedJP1Fill), together with the base cases in JP1.lean, certify a per-instance statement for every even $N$ from 10 to 1000: one decide-checked theorem per value of $N$. These are individual certificates, not a single quantified theorem over the range.

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. It is a deliberately standalone module — a kernel-checked record of the exponent bookkeeping, not an import that other constructions of the project build on.

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{E}\mathrm{H}}_{\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-23 snapshot the layer contains no sorry at all. The last one — the correctness theorem for the search function findGoldbachPair, which had stood since April 2026 — was closed in July by an induction over the function’s well-founded recursion, using the principle Lean generates automatically for such definitions. The statement was not weakened to make it provable: it is unchanged, and only the proof body and its docstring were rewritten.

Two qualifications keep this from being read as more than it is. First, sorry-free is not axiom-free: the 9 axiom declarations listed below are untouched by this, and they are the substantive gaps. Second, the 3 native_decide occurrences in the layer — all in this one file — extend the trusted base from the kernel to the Lean compiler (visible as Lean.ofReduceBool under #print axioms), and are used only for non-load-bearing sample evaluations, never for a result claimed as kernel-checked.

The audit script that produces these numbers now carries an empty allowlist, so any sorry introduced in future is reported as unexpected and fails the check rather than being silently tolerated.

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 formalization package contains BLUEPRINT.md, a map of the open formalization debts together with effort estimates for closing them. Anyone may compare the statements made on this page with the actual state of the code.