A First Proof Sprint

1. Overview and Context

This monograph documents a multi-agent "proof sprint" conducted over approximately 55 hours (February 11–13, 2026) involving ten distinct research-level mathematical problems. The project utilized a hybrid workflow combining rapid draft generation by AI agents (Claude instances and Codex) with adversarial verification, targeted repair, and explicit provenance tracking.

The core methodological innovation is the use of wiring-diagram decompositions, where proofs are represented as typed graphs of claims and dependencies. This structure allowed the system to localize gaps, coordinate reviewer-driven revisions, and distinguish between mathematical status (closed/partial/conditional) and QC-validation status (validation-complete/partial).

2. Methodology

The sprint employed a "Lakatosian" cycle of conjecture, critique, and reformulation, accelerated by AI:

• Agents: A human dispatcher coordinated multiple Claude instances (acting as provers) and Codex (acting as critic and research assistant).
• Workflow:
  1. Drafting: Rapid generation of initial proof attempts.
  2. Adversarial Review: Critics identified overclaims, hidden gaps, and logical inconsistencies.
  3. Targeted Repair: Agents focused on specific "gaps" identified in the dependency graph rather than rewriting entire proofs.
  4. Verification: Node-level verification with predecessor/successor context was used to improve calibration over whole-draft reviews.
• Tooling: The system utilized Python (NumPy/SciPy, SymPy, mpmath, PHCpack, cvxpy) for computational checks, and custom scripts for wiring-diagram generation and pattern tagging.
• Outcome Typing: Results were explicitly categorized as Closed (C), Partial (P), or Conditional (?), with validation status marked as Complete (✓), Partial (∼), or Unvalidated (?).

3. Problem-Specific Results

The sprint addressed ten problems across diverse fields (Stochastic PDEs, Representation Theory, Algebraic Combinatorics, Free Probability, Equivariant Homotopy, Spectral Graph Theory, Geometric Topology, Symplectic Geometry, and Computer Vision).

| Problem | Domain | Status | Key Outcome |
| :--- | :--- | :--- | : |
| P1 | Measure Theory / SPDE | Closed (C/✓) | Proved equivalence of the $\Phi^4_3$ measure under smooth shifts using Cameron-Martin theory and variational construction. |
| P2 | Representation Theory | Closed (C/✓) | Established the existence of a universal test vector (the new vector) for Rankin-Selberg integrals, dependent on a cited theorem. |
| P3 | Markov Chains / Combinatorics | Closed (C/✓) | Constructed a Markov chain (inhomogeneous multispecies $t$-PushTASEP) with the specified ASEP polynomial stationary distribution. |
| P4 | Free Probability | Partial (P/? ) | Proved analytically for $n \le 3$ and via algebraic certificate for $n=4$. The general case for $n \ge 5$ remains open. |
| P5 | Equivariant Homotopy | Closed (C/∼) | Characterized $O$-slice connectivity for $F_O$-local spectra via geometric fixed points. Full indexing-system extension remains open. |
| P6 | Spectral Graph Theory | Partial (P/? ) | Proved for complete graphs ($K_n$) with $c_0 = 1/3$. The general graph case is conditional on a "Barrier Maintenance Invariant" (BMI) bound. |
| P7 | Geometric Topology | Closed (C/∼) | Provisionally closed via a "rotation route" (codimension-2 surgery) for lattices with 2-torsion. Independent ledger re-check pending. |
| P8 | Symplectic Geometry | Closed (C/✓) | Proved that 4-valent polyhedral Lagrangian surfaces admit Lagrangian smoothing via symplectic direct sum decomposition and product structures. |
| P9 | Algebraic Geometry / Vision | Partial (P/∼) | Strong computational evidence for polynomial detection of rank-1 scaling in quadrifocal tensors; universal converse step lacks clean algebraic closure. |
| P10 | Numerical Linear Algebra | Conditional (?/?) | Provided a PCG algorithm for RKHS-constrained tensor CP decomposition, valid under explicit assumptions (e.g., $\lambda > 0$). |

4. Key Contributions

A. Methodological Advances

• Wiring-Diagram Verification: The project demonstrated that representing proofs as dependency graphs allows for more effective gap isolation than narrative drafting. Disagreements became local and repairable.
• Layer-Switching Strategies: In Problem 7, the team successfully pivoted from a "reflection route" (blocked by parity issues) to a "rotation route" (codimension-2), resolving a structural obstruction.
• Adversarial Iteration: The critic-responder loop successfully converted early overclaims into explicit, honest outcomes (e.g., distinguishing between "proven for $n=4$" and "open for $n \ge 5$").
• Structured Handoffs: Unresolved obligations were preserved as named, testable next steps rather than implicit deferrals.

B. Mathematical Contributions

• Problem 6 (Graphs): Provided a rigorous proof for the $K_n$ case of the $\epsilon$-light vertex subset problem ($c_0 = 1/3$) using a barrier greedy algorithm and PSD trace bounds, bypassing complex interlacing family machinery for this specific case.
• Problem 8 (Lagrangian Smoothing): Established a new algebraic argument showing that 4-valent vertices in polyhedral Lagrangian surfaces force a symplectic direct sum decomposition ($R^4 = V_1 \oplus V_2$), which forces the Maslov index to vanish exactly, enabling smoothing without surgery.
• Problem 4 (Free Convolution): Discovered that the superadditivity of root separation energy holds for $n=3$ via a specific identity involving the discriminant, but fails for plain coefficient addition, highlighting the necessity of the MSS bilinear structure.

5. Significance and Limitations

Significance:

• Empirical Validation of AI Math: The sprint serves as an empirical extension of the question "Can computers participate in mathematical reasoning?" It shows that AI agents, under human supervision, can navigate complex research problems, identify subtle gaps, and produce publishable-quality drafts.
• Speed vs. Rigor: The project highlights a persistent asymmetry: generation is fast, but trustworthy validation is slow. The most significant leverage came not from first-pass drafting, but from structured verification tools that made weaknesses visible early.
• Reproducibility: The entire process is version-controlled (Git), with 333 rollout traces and over 965 million tokens processed, providing a transparent audit trail of the "machine-speed" Lakatosian cycle.

Limitations:

• Partial Closure: Several problems (P4, P6, P9) remain partially closed or conditional. The system did not "solve" every problem but successfully bounded the scope of the open questions.
• Dependency on External Theorems: Some "closed" results (e.g., P2, P7) rely on cited theorems or independent ledger re-checks that were not fully re-derived within the sprint.
• Generalization Gaps: Proofs often succeeded for specific cases (e.g., $n=4$ in P4, $K_n$ in P6) where general proofs remained elusive, indicating that current AI capabilities may still struggle with the "leap" required for full generalization in highly abstract settings.

6. Conclusion

"A First Proof Sprint" demonstrates that structure-aware verification and layer-switching strategies significantly improve the reliability and calibration of AI-assisted mathematical research. By treating proofs as modular, verifiable graphs rather than monolithic texts, the system successfully navigated ten research-level problems, producing a mix of closed, partial, and conditional results that are explicitly documented and reproducible. The work suggests a future where human-AI collaboration follows a rapid, iterative cycle of conjecture and critique, accelerating the discovery process while maintaining rigorous standards of proof.