Methodology

Operating principle: asset-forensics + research-probe

The project operates in a strict mode that we call asset-forensics + research-probe. 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 281 claims (snapshot of 2026-07-19). Every claim carries an explicit status and a confidence level. Nothing in the project exists “in the air”: if a statement is mentioned, it is entered in the registry, and its current state is publicly visible.

Status distribution

Confidence levels

The confidence level records how firmly a claim is supported: by a proof, by a source, by a computation, or only by a heuristic.

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. We do not hide this fact; we publish it. 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-19), 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 metric goldbach_proved = 0 is wired into the protocol: while the goal remains open, no experiment may return $1$. This is not pessimism but an honest record of the current state of affairs — the binary Goldbach conjecture is not proved.

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 exact bans of the project

Three bans are stated literally and apply without exceptions. They protect the project against the most common ways of presenting the desired as the actual in this subject.

Ban 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.

Ban 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.

Ban 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 most important trust signal of the project is not its successes but its documented self-corrections. A mandatory red-team protocol applies: strong claims undergo a deliberate attempt at refutation before they receive their status. Below are the actual cases in which this protocol worked against ourselves.

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 to the precise one. Lesson: even one’s own texts are read as hostile.

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

The statement CWC₃ figured for some time as Theorem. Careful review showed that a proof of the required completeness does not exist. The status was downgraded to Conjecture. Lesson: the title “theorem” is expensive, and it has to be taken away.

We regard these records as the main content of this page. A project that cannot exhibit a single case of correcting itself either never errs — which is impossible — or does not look at itself attentively.

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 numerical result is a guaranteed interval, not an approximation with an unknown error. See the Numerical experiments page.

Lean 4, locally and without API calls

Formal fragments are checked by the Lean 4 kernel locally, with zero external API calls: verification depends neither on the network nor on third-party services and infrastructure. 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: what exactly is claimed, what we have verified, and how this affects (or does not affect) the registry statuses is recorded. 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 its solution. It promises that everything said on this site is said with a precisely stated status — and that any error we find will be corrected publicly, with a record of the correction.