Methodology

Operating principle: lemma-driven research

Since July 2026 the project has operated in a lemma-driven research mode: work is organized around one exact theorem dossier at a time, with independent primal, dual, and source-verification roles on hard gates. The earlier asset-forensics + research-probe discipline is preserved as the audit backbone. Every research session must produce at least one of five kinds of output:

• a technical result — a new computational or analytic technique;
• a verified negative — a rigorously documented negative outcome (this path does not lead to the goal, and here is why);
• a citation audit — a check that the sources used say exactly what they are cited for;
• a Lean artifact — a machine-checked formal fragment;
• a strategic clarification — a revision of statuses, priorities, or stopping criteria.

A session that produces none of these is counted as unfinished. The rule is a discipline device: the project cannot absorb unlimited time while leaving nothing behind.

Claim registry

The core of the methodology is a registry of 291 claims (snapshot of 2026-07-23). Every claim carries an explicit status and a confidence level. No statement in the project exists off the record: if it is mentioned anywhere, it is entered in the registry, and its current state is recorded there.

Status distribution

Each claim also carries a confidence level recording how firmly it is supported — by a proof, by a source, by a computation, or only by a heuristic. The counts themselves matter less than the rule: confidence is written down before a claim is used, not after.

Most of the registry is always awaiting re-review — a feature, not a bug. Claims age: a periodic audit requires every live claim to have been re-reviewed within 45 days, while historical claims are allowed to grow stale and are revisited when touched. This fact is published, not hidden. The registry is a living audit: sources are re-checked, and statuses are lowered as well as raised. A frozen, “perfect” registry would be evidence that nobody is watching it.

Reproducible experiments

The project maintains 272 experiments (snapshot of 2026-07-23), each of them a script with canonical metrics. An experiment cannot be “retold in words”: it can only be re-run, yielding the same set of numbers.

Two of the canonical metrics are hard constraints that act as safeguards against self-deception:

The invariant goldbach_proved = 0 is a hard-coded protocol tripwire, not an empirical metric: any automated summary that ever reported $1$ would be, by construction, a bug. It encodes the current state of affairs — the binary Goldbach conjecture is not proved — in a form that scripts cannot accidentally contradict.

The metric no_new_axiom = 1 forbids introducing new axioms for open bridge statements. If a bridge is unfinished, it may not be “completed” by postulation: a bridge is either proved or open. The formal side is described on the Formalization in Lean page.

Guardrails: the project’s standing prohibitions

Three prohibitions are stated literally and admit no exceptions. They guard against the most common ways in which, in this subject, what one hopes for is passed off as what one has proved.

Prohibition I. Never claim Goldbach

No text of the project — paper, note, or code comment — may assert or hint that the binary Goldbach conjecture is proved, “almost proved”, or “practically solved”. The status of the problem is Open problem, and any text violating this is treated as a defect and corrected.

Prohibition II. No axioms for open bridge statements

If a bridge statement is open, it may not be closed by an axiom. Such a “solution” proves nothing and merely hides the problem. An open bridge is marked Open problem and waits for a genuine proof or an explicit parking decision.

Prohibition III. Average / $L^2$ / almost-all results are not fixed-$N$ progress

Results “on average”, in the $L^2$ norm, or for “almost all” even numbers are substantive results of analytic number theory, but they are not progress on the problem for a fixed $N$. The project forbids presenting them as steps toward the binary conjecture: the conjecture asserts something about every even number, not about a majority.

Kill criteria and parking

Every research line has explicit stopping criteria, written down before the line starts. When a line meets its kill criterion, it stops — without renegotiation with oneself.

A stopped line is parked: its state, the reason for stopping, and the conditions for reopening are recorded in the registry. A parked line is not reopened merely because one “feels like trying once more”. Reopening requires new input:

• a new theorem (one’s own or from the literature), or
• a new computation that changes the picture.

This protects the project from endlessly returning to beautiful but dead-end ideas — a classical trap in work on difficult conjectures.

Internal red team: the self-refutation protocol

The clearest evidence of discipline in a project like this is not its successes but its documented self-corrections. A red-team protocol is mandatory: strong claims undergo a deliberate attempt at refutation before they are given a status. The cases below are ones in which the protocol worked against the project itself.

The BK+ documentation overclaim

The documentation of the BK+ work contained a formulation stronger than what the content actually supported. A red-team review detected the discrepancy, and the formulation was corrected. Lesson: one’s own texts have to be read as a hostile referee would read them.

Claims downgraded to superseded

Following red-team review, part of the registry was downgraded to superseded: these claims are not refuted, but they have been replaced by more precise versions and are no longer used as support. Lesson: a status is downgraded as routinely as it is upgraded.

CWC₃: from “theorem” to conjecture — and back, with conditions

The statement CWC₃ figured for some time as Theorem. Careful review (May 2026) showed that a proof of the required completeness did not exist, and the status was downgraded to Conjecture. A subsequent formalization then re-established it at an intermediate rank: CWC₃ is now certified in the project’s Lean layer as a theorem modulo explicit classical inputs, and it is not used as an input to any Goldbach claim. Lesson: the word “theorem” is expensive — it can be taken back, and it is earned again only with the conditions stated in full view.

These records are the substance of this page. A project that cannot exhibit a single case of correcting itself either never errs — which is impossible — or is not looking.

Rigour tools

Trust in the numbers and proofs of the project rests on three technical pillars.

Interval arithmetic (Arb)

Numerical certificates are computed in the interval arithmetic of Arb at 160-bit precision with outward rounding: every certified table is a guaranteed interval, not an approximation with an unknown error. Not all exploratory numerics reach this bar — results that are checked by other means are labelled accordingly and are never silently promoted to certificate rank. See the Numerical experiments page.

Lean 4, checked locally

Formal fragments are checked by the Lean 4 kernel locally, with no network access: verification depends on neither a remote service nor a hosted tool. See the Formalization in Lean page.

About 20 CI check scripts

Roughly twenty check scripts run in CI: from recomputing canonical metrics to controlling the consistency of the claim registry. A broken check blocks changes — statuses are not edited “around” the scripts.

Literature watch

The project runs a weekly triage of new preprints on arXiv over seven thematic profiles — among them sieve methods, dispersion, and the Goldbach problem. Each profile covers its own slice of the literature adjacent to the research lines of the project.

Fresh preprints claiming relevant results undergo dated audits, which record what exactly is claimed, what has been verified here, and how this affects (or does not affect) the registry statuses. The dating is essential: an audit is a snapshot of knowledge on a specific day, not a timeless judgement. The relation to external results and barriers is discussed on the Barriers page.

What distinguishes this project from typical “Goldbach proofs”

The subject of the Goldbach conjecture attracts an enormous number of unverifiable texts claiming a complete solution. This project is built on the opposite principles:

• Public status discipline. Every claim carries a visible status — from Theorem to Open problem and Conjecture — together with a history of its changes. The reader always sees what is proved, what is conjectured, and what is parked.
• Negative results are preserved. A verified negative is a full-fledged result of the project, not an embarrassment. An honestly documented dead end saves the time of everyone who comes after. See the Results page.
• Machine checking. Numbers are certified by interval arithmetic, formal statements by the Lean 4 kernel, and the consistency of the registry by CI scripts. Nothing rests on authorial confidence alone.

The binary Goldbach conjecture remains open Open problem. This project does not promise a solution. It promises that everything said on this site is said with a precisely stated status, and that every error found in it will be corrected in public, with a record of the correction.