Technical Report for AI4Math-2026 Track 2: Mechanically Orchestrated LLM Sub-Agents for Theorem Proving in Lean 4

This technical report describes a pipeline for formal proof generation in Lean 4 that emulates the workflow of a working mathematician: decompose the theorem into sub-lemmas, probe for counterexamples, prove each sub-lemma in isolation, construct from scratch what the library lacks, and assemble the verified pieces under kernel control. Six sub-agents carry out the cognitive work; a deterministic shell state machine handles every coordination decision between them. Diagnostic outputs pass between sub-agents byte-identically, with no interpretive layer. Applied to the ICML 2026 AI4Math Challenge 2 (Theoretical Computer Science Proving in Lean), the pipeline solves 30 of the 34 challenges (600 of 1000 points) in our local Lean verification with no human-in-the-loop interaction at any sub-agent dispatch or coordination decision.