How the ellipsoid
proofs were built.

A public development with explicit statements and checks.

The continuation is published in LLM4Rocq/ellipsoid_fitting_rocq. Its status and reading guide link the mathematical claims to frozen statements, saved proofs and assumption checks. The links below identify particular released commits; the October 2 measurements further down describe an earlier stage.

What changed in verification

Kernel checking establishes that a proof has its formal type. The surrounding checker must also establish that it checked the intended sources, statements and outputs. The phase 13 repair strengthened those connections: it reads Rocq source syntax, records compiler runs and output hashes, compares statements with their accepted versions, and checks resolved names. The annotated release records for phase13, phase14 and shifted report checks in two fresh clones and agreement on all 54 repaired-side regression tests.[10][11][12]

Source review and the note, through 25 October

The updated shifted-sample note cites the release and theorem files. A further documentation commit identifies the replacement of the planned direct singular-value-tail argument by a centered sample-covariance argument, and changes one displayed log d factor to log(p+1) to match the formal estimate. These are documentation changes after the shifted tag.[13]

The rest of this report preserves the September 30–October 2 case study. Its 648-module closure, 801 registered modules, eight-axiom allowance and tool-call totals belong to that period; they are not totals for the later public release.

The evidence supports a useful division of labour and repeated use of interactive feedback. It does not establish how much faster the team was than one agent, whether MCP reduced total cost, or which model would have performed best. No controlled comparison was run.[4]

The original three clauses were proved.
The faithfulness question is separate.

The target is one formal theorem with three main clauses. For independent standard Gaussian points in dimension d, the sample density is n(d)/d². The fitting equation is x_i^TSx_i = d. The statements allow arbitrary sample-size sequences subject to the specified eventual density bounds.[2]

These are summaries of the fixed formal statements, not a new mathematical review of their agreement with the paper. No assertion is made here about the critical density exactly equal to 1/4.

For this report, a fresh read-only audit checked all 648 proof-source hashes, the six frozen-source hashes and the axiom contract against the merged tree. It found no mismatch. The merged tree equals the checked PR head. This audit did not rerun the full Rocq build.[1]

Fix the mathematical interface.
Let the proof decomposition evolve.

The most consequential decision was the change in review scope. The user wanted to review the main theorems and the definitions that give them meaning, rather than a long sequence of intermediate challenges.

On 30 September, the work was reorganized into one main-statement package with three clauses and a shared glossary. A separate session authored the statement; the final results and policy modules were written by the AWS master solver. Internal lemmas could be split, replaced and reassigned while the recorded main statement and its five trusted dependencies stayed unchanged.[2][6]

1. 1Fix the targetMain clauses, Gaussian law, event definitions and quantifier order.
2. 2Assign bounded workOne owner per module family, explicit dependencies and expected conclusions.
3. 3Develop and saveInteractive goals, library searches, tactic trials and saved source proofs.
4. 4Check integrationsCompile, inspect every result’s assumptions, then run the kernel checker.
5. 5Check the exact targetRebuild the final closure and check theorem and policy against the fixed type.

The final step moved from fixed positive densities to arbitrary sample-size sequences by checked padding and monotonicity reductions. This preserved the order “choose the spectral constants, then quantify over all sequences.” The fitting and balanced-alternative clauses were assembled from these limits and the already checked supercritical results.[3][8]

Proof.
  exact (paper_main_results_from_conditioned
           paper_main_conditioned_limit).
Qed.

Three workers, with distinct contributions.

Initially, AWS had the Codex master plus Arthur and Marcol. Lancelot joined later, making three proof workers plus one master. The Mac coordinator handled deployment, recovery and some supervision. The AWS logs also record two short setup/review helpers; they are not counted as mathematical workers here. The recorded AWS model identifiers were gpt-6-astra for the master and claude-opus-5-5 for the three workers. Earlier Cleps work used other model configurations.[4][6]

Attribution follows assignments, worker reports and integration records, not Git author names or raw commit counts. Roles changed over time; this table summarizes their main contributions.[3]

Assessment: all three workers were useful in the ordinary, observable sense: their work survived integration and was consumed by the proof. Parallel work was feasible because module ownership and interfaces were explicit. How much elapsed time it saved remains unmeasured.

Rocq MCP was a working instrument,
not just an installed dependency.

The server, rocq-mcp-evolve, exposed Rocq’s live proof state to the agents. They could open a theorem, inspect its goals, submit tactics, try alternatives, roll back and check a candidate proof. This gave direct feedback on each proposed proof step. The logs establish use, but they do not measure the incremental time saved over a compiler-only workflow.

Unique native MCP tool calls before the proof-completion receipt on 2 October at 13:58 UTC.

Counts come from three explicit primary Claude transcripts, deduplicated by tool-call ID. They include setup tests, retries and proof replay. One call can contain several tactics; repeated openings can target the same theorem. They exclude MCP requests sent through shell scripts, earlier Cleps work and later publication work. Lancelot joined much later, so totals are not a productivity ranking.[4]

The master used a private MCP connection through scripted orchestration, so it has no comparable native-tool count in this table. A separate receipt records successful MCP replay of both conditioned-limit theorems and the final paper_main_results theorem at 13:11 UTC. That receipt still said independent verification was pending, correctly: the final clean check came later.[7]

A useful discrepancy between prescribed and observed practice: the instructions encouraged auto_close first on every new goal, but the counted native sessions contain only four such calls, against 929 opens. The observed workflow was mainly driven by step, try, check and build. This count does not include automation written inside tactics or invoked through shell transports.

A layered toolchain.

The primary transcripts contain 2,033 Arthur Bash calls, 1,656 Marcol Bash calls and 139 Lancelot Bash calls before the cutoff. The master made 2,522 orchestration calls named exec; each could run several commands. These units are not directly comparable. Shell text frequently mentions source search, compilation and Git, but those mentions are not separate executions.[4]

Coordination was real work.

Additional workers increased the number of independent proof lines, but also created dependency, memory and communication work. The journal contains concrete failures rather than a frictionless account of parallelism.

The first three issues are supported by the AWS master and worker records; the communication delay and migration are also documented by the Mac coordinator. The message delay was about two hours, not a measurement of its effect on total completion time.[3][6][7][9]

The final day, in context

1. 30 September

   The review target changes to the three main statements. Earlier proof libraries and other branches remain available for reuse.

2. 1 October

   AWS takes over after recovery from Cleps. The master, Arthur and Marcol work on separate proof families under a common environment.

3. 2 Oct · 11:28

   Lancelot receives its first mathematical assignment. Its first scalar module is checked by about 11:51; the second is reported checked at 12:18.

4. 2 Oct · 12:37

   Lancelot delivers the composition review, including the cast-conversion finding. Lower-law and conditioned-limit integration continue.

5. 2 Oct · 13:23

   The final theorem and policy are saved and kernel checked. The clean exact-type check is still pending, and the journals say so.

6. 2 Oct · 13:55

   The clean 648-module check passes. Completion is recorded shortly afterward; the user merges the published result at 14:35.

This is the final development phase, not a claim that the whole paper was formalized from scratch in a day. It relied on an existing library and earlier human-directed and agent-generated work.

A successful case study,
not a controlled experiment.

Tool counts measure interaction, not mathematical progress. A difficult theorem can require many unsuccessful calls; a short assembly proof can depend on hundreds of earlier results. Module and commit counts are similarly unsuitable as stand-alone productivity measures.

Recommended method for a future formalization

Keep one stable main-statement package and a small human review surface. Use a proof-writing master with two substantial workers, adding a third when a concrete independent task is ready. Give each worker its own source tree and proof state. Prepare dependencies, require task acknowledgements, and budget memory before adding concurrency. Keep compiler and kernel checks separate from interactive diagnostics.

To evaluate efficiency rather than only completion, record task start/finish times, dependency waiting, failed attempts, model usage and integration time from the beginning. Compare matched bounded tasks with and without MCP, or with one versus several workers. Treat the present evidence as motivation for those experiments, not as their result.[9]

How the accounts were checked.

The original October 2 audit was read-only on AWS. It inspected completion records, selected saved proofs, journals and four explicitly identified primary session logs. It did not message the proof agents, change their work, or rerun the full compiler pipeline. This public copy presents the aggregate measurements and includes the source-hash check, merge receipt and kernel/audit log. The other historical receipts, transcript excerpts and measurement inputs remain in retained project records; they are not included in this package. Sources 1–9 concern that original account. Sources 10–13 identify the public continuation; this page update did not rerun its proofs.

1. Final proof verification and source audit

   Recorded proof verification (retained project record; not included in this public package), clean-check log (retained project record; not included in this public package), kernel/audit log, this report’s source-hash check, and merge receipt. The record reports no unexpected axioms, zero holes and exact theorem/target checks. Its proof-time regression results include 38 tests, 45 draft-review records and zero broken links. The library retains 22 historical lint warnings; “zero warnings” applies only to the final exact-type check.

2. The fixed statement and its interpretation

   In the private repository LLM4Rocq/ellipsoid_rocq, at the merged commit df283b79: analysis/challenges/paper_main_results/Challenge.v, the challenge metadata analysis/challenges/paper_main_results/challenge.json and the main definitions analysis/PaperMainDefinitions.v. The admitted statement placeholder is a specification, not part of the submitted solution closure. That repository is not public, so these files are named without links.

3. Task ownership, checked contributions and completion

   AWS MASTER_JOURNAL.md, arthur-report.md, marcol-report.md, lancelot-report.md, and the committed progress record analysis/reports/MAIN_PROOF_PROGRESS.md (private repository, commit df283b79). Selected dated excerpts and source hashes were inspected in the source collection (retained project record; not included in this public package). Later completion records supersede earlier “pending” entries without erasing them.

4. Session-level usage audit

   Aggregate counts and exact scope (retained project record; not included in this public package), reproduced by collect_usage.py (retained project record; not included in this public package). The cutoff is the completion receipt at 13:58:26 UTC. Calls are counted once per ID; no malformed lines or duplicate tool-call IDs occurred in the selected records. Guardian/helper transcripts, the Mac coordinator and Cleps are excluded. File hashes identify the inspected logs, but raw logs remain private on AWS. PROOF COMPLETE text is not counted as a distinct accepted theorem.

5. Lancelot’s bounded composition and artifact review

   The L2 review identified the natural/real cast bridge; its later update marked it resolved. The L3 review independently checked the closure and final source/receipt consistency without claiming human review. See the audit excerpts (retained project record; not included in this public package) and the final lower-probability source analysis/PaperMainSquarefreeLowerProbability.v (private repository, commit df283b79).

6. Historical methods and operational record

   The methods notebook analysis/reports/AUTOFORMALIZATION_METHODS.md (private repository, commit df283b79) and Mac coordinator journal document library bridges, MCP diagnostic limitations, recovery, environment setup and the message delay. Relevant passages were inspected in the source collection (retained project record; not included in this public package). They are dated observations, not current-status summaries.

7. Actual MCP proof evidence

   Master’s final theorem replay (retained project record; not included in this public package) and Lancelot’s real-import and whole-module check after reconnect (retained project record; not included in this public package). These records support MCP use; final proof acceptance at the fixed type is established separately by source [1].

8. The final composition in saved code

   The modules PaperMainConditionedLimit.v, PaperMainConditionedFromLower.v, PaperMainFixedLowerProbability.v, PaperMainResults.v and PaperMainPolicy.v in analysis/ of the private repository LLM4Rocq/ellipsoid_rocq, at the merged commit df283b79. The commit identifies the merged bytes, not moving branch tips.

9. Official workflow documentation, not project-performance evidence

   OpenAI’s subagent guidance describes independent tasks and the coordination cost of concurrent edits. Its steering and queueing documentation explains the message-delivery distinction. These sources informed terminology and recommendations; they do not prove any speedup in this run.

10. Public phase 13 release and checker repair

    Tag phase13 identifies f16e6a263f8579f7f2a794537ee194d78842cafe. See its README, checker and repair commit. The tag message records the final fresh-clone and regression results; paths to retained evidence in that message do not imply that its raw logs are public.

11. Public phase 14 statements and proofs

    Tag phase14 identifies 5f81a422a9b430f98a3ae8be97fdd9f2ae91e8f7. Compare the PSD-rank statement with its theorem, and the lift statement with its theorem. The rank bound has the form 2^n <= r^K for sufficiently large even n; the files give the precise quantifier order.

12. Public shifted-sample statements, proofs and checks

    Tag shifted identifies 305747af48d4f75e26378888a8111d591145fa52. The README maps all seven statement files to the corresponding proof files. The identity checks apply each theorem at its frozen statement type. The release adds 23 library files and records checks in two fresh clones.

13. Public documentation changes on October 25

    The release citations and the proof-route and logarithm correction change documentation only. They leave the shifted tag and its proof sources unchanged. The latter commit records the D2 source-review finding; the separate bounded second-reading report is retained in project records, not published with this page. A third commit, the row-size condition and the reindexing statistic, corrects one table row of extension/README.md and the header comment of extension/Shifted/SparseDimensions.v after that second reading. It changes no Rocq statement or proof.