Methods

Demonstrandum coordinates AI reasoning systems for problem selection, sustained attack, adversarial internal review, and machine verification. Its architecture is proprietary. Erlbacher directs the work, reviews every accepted result, and takes responsibility for the claims.

No result is accepted on a model output alone. Each is reduced to an independently checkable artifact: a kernel-checked Lean proof, an exact certificate checked by independent implementations, or independently implemented exact computations. The applicable grade is stated with the result.

Verification

Kernel-checked. The claim is a Lean 4 theorem accepted by the Lean kernel, with its axioms audited and no sorry. The project record identifies the declaration, pinned toolchain, dependencies, and axiom report.

Dual-checker certificate. A finite witness is accepted by at least two independently implemented exact checkers. Mutation testing is reported where applicable.

Audit-panel. A runnable checker is supplemented by independent recomputation or adversarial review when a second on-disk implementation is absent. The limitation is disclosed with the result.

Limits of verification

Statement fidelity

Mechanical verification establishes the formal claim presented to the checker. Its fidelity to the cited informal statement is reviewed and reported separately.

Novelty

Verification does not establish novelty. Literature searches and their scope are separate parts of the record.

External refereeing

Internal review is not external refereeing. Each project states its review status.

Corrections

Corrections are never silent. A corrected claim retains or links its original text and records the date, reason, and replacement.

12 July 2026 — The strong-majority project page and census README cited an approximately 530-million-graph exploratory sweep whose bulk outputs were not included in the released artifact and lacked a compact published manifest. We removed that unsupported public count. The replacement cites only the released, reproducible census: 268,478 admissible graphs through nine vertices and 89,771 connected 4-regular graphs at orders 10, 12, and 14. No theorem claim is affected.

12 July 2026 — The strong-majority pages and paper v1 stated that mathlib contained no edge-coloring theory at our pin. mathlib in fact contains SimpleGraph.EdgeLabeling (edge labelings, without properness theory), and a proper edge-coloring API is in development (mathlib4#33313). Corrected throughout the same day; no mathematical claim is affected.