Breach: An Interactive Adversarial Agent for Bounded Mathematical Claim Falsification

Large language models are increasingly used to reason about mathematical claims, but their outputs provide no guarantee of correctness: an LLM can produce a proof that is fluent, well-structured, and wrong. We present Breach, a system that inverts the usual framing of LLM-assisted verification. Rather than asking a model to confirm a claim, Breach treats every claim adversarially: it attempts to construct a counterexample using deterministic solvers (Z3, SymPy), using the language model strictly as a translator from informal language into solver-checkable form. All verification decisions are made by the solver, never by the model. Breach reports one of three outcomes for every claim — a concrete counterexample, an honest statement that no counterexample was found within a declared search bound (explicitly not a proof of truth), or a classified “unknown” with a specific, scored reason the solver could not decide. Beyond this base verification loop, Breach introduces two features we believe are novel relative to existing LLM-plus-solver systems: an interactive, step-targeted challenge mechanism that lets a user contest a specific part of the reasoning and receive a response addressed to that exact objection, and an automated “proof autopsy” that, given a counterexample, identifies which step’s implicit assumption it violates and offers to patch and re-verify the claim. We validate Breach against a 22-case corpus curated from the miniF2F benchmark, achieving correct verdicts on all executable cases after fixing one early source of translation non-determinism, which we document transparently. We position Breach precisely against prior work in LLM-assisted formal reasoning and state clearly what it does not attempt: open-ended proof construction, and resolution of genuinely open mathematical problems.