What can a mathematical swarm prove about its own work?
一个证据优先的 Astra 数学蜂群如何从“流畅但错误”走向可审计的研究地图。
2026-09-15 · No theorem claimedThe question is a family of questions
“Cosmic censorship” sounds binary: do singularities hide behind horizons? Mathematically, the answer depends on which statement is being asked. Weak cosmic censorship (WCC) concerns visibility from infinity. Strong cosmic censorship (SCC) concerns extendibility across a Cauchy horizon. Even SCC splits by regularity: a C0 extension allows continuous metrics, while C2 inextendibility controls curvature. Vacuum, scalar-field, spherical, axisymmetric and generic 3+1 settings are different problems.
The swarm’s first useful act was therefore not proving a slogan. It was pinning down which tuple a claim belongs to.
When fluent output failed, the audit became progress
The historical pilot completed five role calls and four independent reviews. Its first formulation sounded authoritative, but the reviewers found structural errors: WCC and SCC were merged; C0 and C2 were treated as interchangeable; “generic” data and the visibility notion were left unspecified; citations were not tied to exact theorem scope.
The old run recorded 592 finished group instances (145 formulation, 148 literature, 150 numerics, 149 audit). Those numbers describe a workflow, not a result count.
The research map that survived review
The dependency is the main scientific artifact: definitions and source scope precede computation. Numerics cannot repair an ambiguous formulation.
Three distinctions that prevent overclaiming
Visibility ≠ curvature
A causal boundary can be visible in a coordinate or conformal picture without proving that curvature invariants diverge.
C0 ≠ C2
Continuous extendibility and curvature-controlled inextendibility answer different SCC questions.
Calibration ≠ genericity
A spherical Einstein–scalar run can test diagnostics, but it does not establish generic 3+1 behavior.
What is actually reproducible?
A frozen 27-fixture regression suite reports TP=17, FP=0, TN=10, FN=0. That is a software regression result for fixed fixtures. It is not a physical theorem. A separate formulation pinning check exposed drift:
That difference is precisely why the evidence ledger records source, claim, assumptions, class, and “does not prove” fields. The map validator is VALID; N1 remains LOCKED; no theorem is promoted.
A timeline with a deliberate stop
classes + gates
5/5 roles
4/4 reviewers
historical traces
collaborator handoff
The remote controller, supervisor and workers are now stopped. Historical DeepSeek runners remain for provenance only; they are not active launchers.
What a mathematician should do next
Pick one narrow formulation family. Verify the primary theorem statement line by line. Pin the data class, asymptotics, visibility and regularity. Then decide whether a calibration or proof-oriented computation is worth funding. The right success metric is a checked claim ledger with independent diagnostics, not worker count, token spend or artifact volume.
That is a smaller promise than “the swarm solved cosmic censorship.” It is also a promise a collaborator can inspect.