// leak
Leak is the proving engine behind CompeteMath. When a problem here is marked verified, a Leak prover wrote a proof in Lean 4 and the Lean kernel checked it.
Rather than being a single program, Leak consists of many experimental pipelines designed to test different approaches to automated theorem proving. Currently, we operate five main agent harnesses, all driven by Anthropic’s Claude Sonnet 5 CLI Agent.
These harnesses differ in the tools they are allowed to use, how they interact with the Lean kernel, and their underlying proof strategies.
A Claude Sonnet 5 agent forced to prove a theorem one-shot with no compiler feedback or internet search, invigilated by Leak-IV. This harness is highly significant as a baseline control: it failed comedically at FATE-X, agreeing with the findings by the authors of FATE-X, proving exactly why iterative feedback loops are necessary.
The best performing harness of this project. A Claude Sonnet 5 agent forced to continuously try to prove a theorem with no internet search, but granted access to Leak-I and Leak-IV, invigilated by a seperate Leak-IV gate, and allowed to use tools and think for itself. This minimalist but persistent pipeline is significant because it achieved a breakthrough score of 38/98 on FATE-X.
A Claude Sonnet 5 agent forced to continuously try to prove a theorem with no internet search, but given access to Leak-I, Leak-II, and Leak-IV, invigilated by a seperate Leak-IV gate. This harness was designed specifically to test the benefit and reasoning impact of an upgraded pantograph service.
A family of Claude Sonnet 5 agent harnesses utilizing different strategies, but all attempting to construct a have-based proof skeleton for a theorem. Stronghold is significant because it performed highly efficiently in production, successfully proving the vast majority of the CompeteMath practice problem roster.
A spin on the architecture from the goedel-architect prover, making use of Leak-XI, Leak-XII, and Leak-XIV. While the underlying architecture is provably excellent, this harness is significant for demonstrating that the design actually performs worse when driven by a slower agentic loop, compared to other strategies such as Leak Control-II, in contrast to Goedel-Architect's performance when driver by a fast LLM such as Deepseek Flash V4, and compared to other LLM based pipelines.
The agent harnesses do not interact with Lean directly. They rely on specialized Model Context Protocol (MCP) services to navigate the library, manipulate proof states, and compile results.
Lemma search over Mathlib. The agent describes the shape of the required theorem, and the service retrieves existing declarations so the prover builds on the library rather than reinventing it. (Leak-XI targets a newer toolchain than Leak-I).
An interactive Lean proof-state daemon. The agent can open a goal, apply a tactic, and observe the resulting state difference before committing to a path—providing vital execution feedback.
A graph-based elaboration service used primarily by Ultra. It validates dependency graphs and elaborates individual declarations so the prover can verify exactly what a specific name means.
The final compilation gate. These services compile the completed proof script against the Lean kernel. A proof is only accepted if it passes with zero warnings, ensuring unfinished proofs never slip through. (Leak-XIV targets a newer toolchain than Leak-IV).
To maintain a consolidated codebase and simplify deployments, the experimental pipelines and harnesses do not live in separate repositories.
The code for all five harnesses, along with their prompts and MCP tool configurations, is open-source and available directly within the main CompeteMath infrastructure repositories.