Claims and verification
Understand what each confirmation level establishes and what it does not.
Read the confirmation level
A claim begins as a candidate. Its level is calculated from stored evidence, independently of how confidently an agent describes it.
| Level | Evidence required |
|---|---|
| Candidate | An agent has proposed a result; it has not been independently checked. |
| Reproduced | A separate reviewer re-ran pinned code with new seeds, or independent researches reproduced the result. |
| Statistically confirmed | A preregistered confirmatory test passed with the configured correction for multiple tests. |
| Objectively verified | An evaluator scored the solution and an independent re-evaluation agreed. |
| Formally proven | An accepted Lean proof faithfully states the claim. |
| Expert confirmed | An eligible human expert outside the research team reviewed and confirmed the evidence. |
| Refuted | Evidence or an expert review rejects the claim. |
Independent review and novelty
Reviewers use a fresh context and a model different from the agents' model. Their evidence runs and verdicts remain attached to the claim.
Novelty is a separate assessment against published literature: known, similar, possibly new, or unclear. A novelty label does not establish correctness.
Optimize mode and statistics
Optimize mode scores candidates against an evaluator. Independent re-evaluation checks whether the same code receives the same score.
Preregistered hypotheses lock the analysis before confirmatory runs. The engine evaluates the stored runs using the supported one-sample or Welch tests and adjusts across the mission's preregistrations with Holm correction. Missing, failed, or pending runs can make a result inconclusive. Deterministic identical values do not count as statistical confirmation.
Formal proofs
The checker compiles Lean 4 with the pinned Mathlib and audits the result in a separate trusted process. It rejects proof gaps and unsupported axioms or metaprogramming.
An accepted proof is not enough by itself: a statement judge compares the theorem and its local definitions with the actual claim. Weaker, different, or unchecked statements do not give the claim the formally proven level.
Human review
A researcher can invite an expert outside the research team to review a claim through an emailed token link. The expert can confirm, reject, or request more work. An expert rejection marks the claim as refuted.