Breach: An Interactive Adversarial Agent for Bounded Mathematical Claim Falsification

Introduction

Large language models can produce mathematical arguments that read as coherent, well-formatted proofs while containing subtle logical errors — an unstated assumption, a case silently omitted, an inequality that fails at a boundary value. Because the surface form of a hallucinated proof is often indistinguishable from a correct one without independent checking, naively trusting an LLM’s self-reported confirmation of a mathematical claim is unsound.

A natural response, pursued by a growing body of work, is to pair an LLM with a formal or semi-formal verification backend: the model proposes or translates, and a deterministic system checks. We adopt this general pattern, but invert its usual orientation. Most LLM-plus-solver systems are framed around proving: given a claim believed true, construct a certificate of that truth. We instead frame the system around disproving: given any claim, actively search for the specific case that breaks it, and only report success in finding none as a bounded, explicitly non-definitive result.

This adversarial framing has two practical motivations. First, it is a more honest default: a system whose only mode is “attempt to confirm” has every incentive, architecturally, to produce a confirmation, whereas a system whose only mode is “attempt to break” has no comparable failure mode toward false confidence. Second, it matches how working mathematicians and engineers already use SMT solvers and computer algebra systems in practice — not to construct an entire proof mechanically, but to mechanically clear specific, checkable sub-claims and hunt for edge cases that are difficult for a human to anticipate exhaustively by hand.

We present Breach, a system built around this adversarial loop, with three further contributions beyond the base architecture:

1. Scored, classified honesty. When Breach cannot resolve a claim, it does not return an undifferentiated “unknown.” It classifies the reason (solver timeout, claim lies outside a decidable fragment, the translation itself was ambiguous, or the claim requires arithmetic the backend cannot express), attaches a confidence score to that classification, and states in plain language what would help resolve it.

2. An interactive challenge mechanism (the “blackboard”). A Breach session maintains a persistent proof state across turns rather than answering once and discarding context. A user can contest a specific step of the system’s reasoning; Breach must respond to that exact objection, either conceding it (triggering a re-verification with the objection encoded as an added constraint) or explaining why the step survives it.

3. Automated proof autopsy. Given a discovered counterexample, Breach attempts to localize which step’s implicit, unstated assumption the counterexample violates, states that assumption explicitly, and offers to add it as a constraint and re-check — closing the loop from “here is why your claim is false” to “here is the minimal fix, verified.”

We are explicit, throughout this paper, about what Breach is not. It does not perform open-ended formal proof construction — the task underlying systems such as DeepSeek-Prover, GPT-f, and AlphaProof, which generate the full sequence of steps proving a true statement inside a kernel such as Lean’s. It does not resolve genuinely open mathematical problems; we discuss this limitation concretely in § 6, including Breach’s explicit, user-facing refusal to treat an unbounded open conjecture (e.g. the Collatz conjecture) as anything other than out of its scope. Breach’s competence is bounded, mechanically decidable claims — a real and useful category, but a narrower one than “mathematical reasoning” at large.

The remainder of this paper is organized as follows. § 2 situates Breach against the most directly related prior systems. § 3 describes Breach’s architecture. § 4 describes the interactive challenge mechanism and proof autopsy in detail. § 5 presents our validation methodology and results. § 6 discusses limitations. § 7 concludes.

Related Work

Work combining large language models with deterministic verification backends for mathematical or logical reasoning has grown substantially. We organize the most directly relevant prior systems along two axes: the general pattern of LLM-to-solver translation, and the narrower subset of systems specifically oriented toward falsification/counterexample discovery rather than proof construction.

LLM-to-solver translation as a general pattern. ProofOfThought (Ganguly et al., arXiv:2409.17270) is a neurosymbolic reasoning framework addressing the lack of interpretability and guaranteed verifiability in raw LLM reasoning. It uses a custom interpreter to parse LLM-generated “thoughts,” expressed as DSL code, into First-Order Logic programs, which a Z3 theorem prover then verifies; an intermediary JSON-based DSL bridges the LLM’s output and the formal verification layer. Ironproof (Blain, arXiv:2610.11073) applies a structurally similar pattern to a different domain: verifying the semantic equivalence of LLM-translated COBOL-to-Python code via Z3-encoded equivalence checking, emitting a machine-checkable certificate when no divergence is found. Both systems share Breach’s core commitment that an LLM alone provides no correctness guarantee and that a deterministic backend must make the actual verification decision; neither, however, maintains a persistent, multi-turn proof state that a user can interrogate, nor offers an automated mechanism for diagnosing why a specific verification failed at the level of an individual reasoning step.

Falsification-oriented systems. Two more recent systems adopt Breach’s disprove-first orientation directly, within the Lean 4 formal proof ecosystem. The /disprove command in the lean4-skills toolkit runs a bounded, six-phase search cycle — profiling the target, consulting prior knowledge, selecting a disproof method from a registry (decision procedures, finite enumeration, random sampling, or external SAT/SMT queries), searching for a witness, and assembling a certified negation term — reporting RE-FUTED only once Lean’s kernel accepts the constructed counterexample, and otherwise distinguishing an uncertified candidate witness from a search that found nothing at all. Li et al. (“Learning to Disprove: Formal Counterexample Generation with Large Language Models,” arXiv:2603.19514) address the same underlying problem from a model-training perspective: they fine-tune LLMs specifically to propose counterexamples accompanied by Lean-verifiable proofs, using a symbolic mutation strategy that generates training data by systematically weakening provable theorems into falsifiable variants.

Positioning Breach. Breach shares its central philosophy — actively searching for falsification rather than defaulting to confirmation — most closely with these two Lean-based systems. It differs from both in two respects. First, architecturally: Breach targets informal, natural-language claims as its primary input and uses general-purpose SMT/CAS backends (Z3, SymPy) rather than operating inside a formal kernel. This trades the Lean-kernel-level certification guarantee these systems provide for substantially broader applicability, at the cost of relying on the correctness of the LLM’s translation step rather than a kernel-checked proof term. Second, and more centrally to this paper’s contribution: neither Lean Disprove nor the fine-tuning approach of Li et al. offers an interactive mechanism for a user to contest a specific step of the system’s own reasoning mid-session, nor an automated procedure for localizing a counterexample to the specific unstated assumption it violates. We are not aware of prior work combining the disprove-first verification philosophy with this degree of interactive, step-level argumentation and automated failure diagnosis; we present this combination as Breach’s primary contribution, and are explicit that the underlying translate-then-verify architecture itself is not novel.

We explicitly distinguish Breach from the separate line of work on open-ended formal proof construction (DeepSeek-Prover, GPT-f, AlphaProof, and related systems trained or searched to generate a full Lean proof for a true statement). These systems address a different and, by current published benchmarks, substantially harder problem — the strongest reported systems resolve on the order of a quarter of miniF2F-style problems at pass @ 1 — and Breach makes no claim of competing with or subsuming this line of work.

System Architecture

Breach’s design rule is a strict separation between translation (handled by an LLM) and verification (handled by deterministic solvers), enforced at the module level: all business logic resides in a small set of core modules, and both user-facing interfaces (a command-line tool and a web application) are deliberately thin renderers over that shared core.

Core verification loop (engine.py). Given an informal claim, a single LLM call translates it into a structured representation: a choice of backend (Z3 for integer/logical claims, SymPy for continuous/algebraic claims), variable declarations with explicit bounds, constraints, and the claim expressed as a checkable predicate. The chosen backend then attempts to find a counterexample within the declared bound. A result is one of: counterexample_found (with the exact witness values), no_counterexample_in_bound (explicitly annotated as not a proof of general truth), or unknown, in which case a second LLM call classifies the failure reason (timeout, undecidable fragment, translation ambiguity, or unsupported backend arithmetic) with an associated confidence score. Every solver invocation is wrapped in a timeout to guarantee the system never hangs indefinitely.

Shared memory (memory.py). A lock-guarded store keyed on claim and task type ensures that repeated or parallel verification tasks are never duplicated or silently overwritten; a write to an already-populated key is rejected rather than overwriting prior work.

Worker dispatch (orchestrator.py). Verification tasks are routed to one of three specialized workers — symbolic (SymPy), constraint (Z3), or numeric (high-precision arithmetic) — implemented as plain function dispatch rather than independent autonomous agent processes, each writing results through the shared memory layer described above.

Bounded parallel search (cases.py). For claims whose search space admits it, Breach can partition the space into independent sub-cases (“cubes”), detect and eliminate cubes that are equivalent under a structural symmetry (e.g. variable permutation or sign flip) before dispatching the remainder in parallel across worker processes, and emit a search certificate recording the total cases generated, the number eliminated by symmetry, worker count, and wall-clock time. This architecture mirrors, at a scale appropriate to a single machine, the cube-and-conquer plus symmetry-breaking technique used in the 2016 resolution of the Boolean Pythagorean Triples problem. We are explicit, both in the system’s own output and in this paper, that Breach does not replicate that result’s scale (the original search covered approximately $2^{7825}$ cases across 800 cores over two days) — only the architectural pattern, demonstrated at a scale a single machine can execute in well under a second.

LLM provider layer (llm_client.py). The only network-dependent component in the system. A provider chain attempts Groq first, falls back to Google’s Gemini API, and falls back again to a locally-hosted Ollama instance if neither remote provider is available, so that the system’s network dependency is a resilience property rather than a hard requirement; a reduced offline translator permits a degraded mode of operation with no API key configured at all.

Interfaces. The CLI (cli.py, built on Typer) exposes check, chat (a persistent interactive session), challenge, export, search, and examples commands, plus an in-session /web command that serializes the current session to a shared state file, launches the web interface as a background process, and keeps the terminal session live — both interfaces subsequently read and write the same state file, so a step challenged in one view is reflected in the other within a short interval. The web interface (web.py, built on Streamlit) exposes a canvas for hand-drawn claims (transcribed to formal text via a vision-capable LLM call and always presented to the user for confirmation before any verification occurs, per the system’s stated policy of never silently guessing at ambiguous input), a chat view, and an export/citation panel.

Interactive Challenge and Automated Diagnosis

The persistent proof state (“the blackboard”)

A Breach session maintains a ProofState object across turns: the original claim, its symbolic translation, an ordered list of reasoning steps (each independently markable as unchallenged, challenged, or resolved), the current verdict, any discovered counterexample, and any citations retrieved for the claim’s mathematical area. This state is never discarded between turns within a session, and is explicitly round-tripped as JSON to allow the CLI and web interface to share one live session.

Step-targeted challenge

A user may contest a specific step by its index, supplying a free-text objection. The system constructs an LLM prompt containing the full ordered step list, the specific step under contest, and the user’s objection, and requires the model to respond specifically to that objection: either conceding that it identifies a genuine gap (in which case the objection is encoded as an additional constraint and the underlying claim is re-verified by the solver) or explaining, with reference to the existing variable domain constraints, why the step survives the objection. The step’s status is updated to resolved and the response is attached to it, persisting in the session state.

Automated proof autopsy

When a claim resolves with counterexample_found, a further LLM call is made — again, strictly for natural-language diagnosis, with the counterexample’s validity already established by the solver, not by this call — asking the model to identify which step of the proof’s reasoning implicitly assumed something the counterexample violates, and to state that assumption explicitly. If no step can be confidently implicated (for instance, if the counterexample directly falsifies the claim with no intermediate reasoning gap at fault), the system reports this rather than fabricating a diagnosis. Where an assumption is identified, the user may accept a system-offered patch: the missing assumption is added to the claim’s constraint set and the solver re-runs, reporting either that no counterexample remains within the (now tightened) bound, or presenting the next counterexample the patched claim still admits.

Validation

A note on repository state. The validation corpus described in this section reflects work completed after this system’s initial hackathon submission. The publicly judged repository snapshot, frozen for competition evaluation, reflects an earlier 5-case validation set; the expanded 22-case corpus reported here is preserved at a fixed, permanent reference point and will be merged to the default branch once hackathon judging concludes, to avoid altering a submission under active evaluation: https://github.com/SoumalyaSaha/Breach/tree/validation-v1.0.

Methodology

We validate Breach against a corpus of problems drawn from miniF2F (Zheng, Han, and Polu, “miniF2F: a cross-system benchmark for formal Olympiad-level mathematics,” arXiv:2109.00110), selecting specifically the subset of miniF2F’s algebra and number-theory problems that fall within Breach’s intended scope — bounded claims admitting a decidable or well-scoped formalization — rather than miniF2F’s full benchmark, most of which targets open-ended formal proof construction and is explicitly out of scope for Breach by design (§ 1). We supplement this with a small number of control cases: claims constructed to be straightforwardly false, included to confirm the counterexample-finding path functions correctly on realistic-looking but incorrect input, not only on true claims.

For each case, we record the expected ground-truth verdict (established independently of Breach, either by direct symbolic/arithmetic verification or by reference to the historical record for cases drawn from known mathematical history), run the corresponding breach check command three times, and record the verdict returned on each run. A case is reported as stable if all three runs agree; any disagreement is investigated and reported, not discarded.

Results

The corpus comprises 22 executable cases plus one case (the Pólya conjecture, BVC-004) included for historical/narrative context only and never executed, since its counterexample ($n = 906,150,257$, per the historical record) lies roughly four orders of magnitude beyond any laptop-scale search and must not be represented as a Breach result.

Across all 22 executable cases, Breach returned the correct verdict in every run reported in Table 1: 18 cases where the ground-truth claim is true correctly returned no_counterexample_in_bound, and 4

ID	Problem	Category	Expected	Observed (3/3)
BVC-001	amc12_2000_p11	algebraic identity	TRUE	No CE
BVC-002	mathd_numbertheory_618	number theory (gcd)	TRUE	No CE*
BVC-003	mathd_algebra_487	algebraic system	TRUE	No CE
BVC-004	Pólya conjecture (1919)	historical context only	—	not executed
BVC-005	control: $a^2+b^2 \ge2ab+1$	control (false)	FALSE	CE found
BVC-006	mathd_algebra_141	algebraic identity	TRUE	No CE
BVC-007	mathd_algebra_160	linear system	TRUE	No CE
BVC-008	mathd_algebra_412	linear system	TRUE	No CE
BVC-009	mathd_algebra_44	linear system	TRUE	No CE
BVC-010	mathd_algebra_126	linear equation	TRUE	No CE
BVC-011	mathd_algebra_398	algebraic identity	TRUE	No CE
BVC-012	mathd_algebra_107	algebraic identity	TRUE	No CE
BVC-013	mathd_algebra_455	linear equation	TRUE	No CE
BVC-014	mathd_algebra_440	linear equation	TRUE	No CE
BVC-015	control: $n^2+n+41$ primality	control (false)	FALSE	CE found
BVC-016	control: $n^2-n$ divisibility	control (false)	FALSE	CE found
BVC-017	control: $a^2+b^2 \ge2ab+2$	control (false)	FALSE	CE found
BVC-018	algebra_sqineq_unitcircat bpamblt1	inequality	TRUE	No CE
BVC-019	algebra_sqineq_36azm9asqle36zsq	inequality	TRUE	No CE
BVC-020	mathd_algebra_388	linear system	TRUE	No CE
BVC-021	mathd_algebra_176	algebraic identity	TRUE	No CE
BVC-022	mathd_algebra_327	inequality	TRUE	No CE
BVC-023	mathd_algebra_24	linear equation	TRUE	No CE

cases constructed to be false (BVC-005, BVC-015, BVC-016, BVC-017) correctly returned counterexample_found with a valid witness in every instance. The corpus spans algebraic identities, linear systems and equations, inequalities, and number theory, drawn predominantly from miniF2F’s algebra split, supplemented by constructed false-claim controls.

A documented instance of translation non-determinism

One case, BVC-002 (mathd_numbertheory_618: for positive integer $n$, if $p(n) = n^2 - n + 41$ and $\gcd(p(n),p(n+1)) > 1$, then $n \ge41$ — a claim whose first true witness is independently known to be exactly $n = 41$), exhibited non-deterministic behavior during initial testing. Across six early runs of the identical input, four returned the correct verdict (no_counterexample_in_bound), one returned unknown classified as translation_ambiguity (confidence 0.92) with the solver reporting that the LLM-generated Z3 formula was syntactically invalid, and one returned unknown classified as timeout (confidence 0.95), where a wider search bound chosen in that particular translation made the nonlinear divisibility search computationally expensive enough to exceed the solver’s time budget.

We root caused this to the absence of any validation or retry step when the LLM’s generated solver encoding failed to parse or proved intractable: the translation step re-generated a fresh encoding on every call with no check that the result was both syntactically valid and tractably bounded before handing it to the solver. We added such a validation-and-retry step and re-verified the case: subsequent repeated testing, including the three runs reported in Table 1, returned the correct verdict deterministically.

We report this finding in full, including the pre-fix failure modes, rather than silently presenting only the post-fix result, for two reasons. First, transparency about failure modes discovered during testing is consistent with the system’s own design principle. Second, and more substantively, the finding is itself evidence in Breach’s favor: at no point across the six pre-fix runs did the non-determinism produce an incorrect confident verdict. Every unresolved run reported an honest, specifically classified unknown rather than a wrong answer presented with false confidence — the system’s honesty mechanism functioning as designed even when the underlying translation pipeline itself was unreliable on this input.

Qualitative evaluation of the interactive mechanisms

The corpus and results above measure only the base verification loop: translate, search, report a verdict. Breach’s interactive mechanisms — the step-targeted challenge loop and the automated proof autopsy — are not captured by a single-shot accuracy table, since their value lies in the quality and specificity of a multi-turn interaction rather than a binary correct/incorrect outcome on one input. We report one representative worked example here as a qualitative demonstration, distinct in kind from the quantitative results of § 5; a dedicated quantitative evaluation of response quality across many challenge interactions is identified as future work in § 6.

Worked example. The user submitted the claim “is $(a-b)^2 > 0$” via the system’s drawn-input interface (transcribed from a hand-drawn sketch and confirmed by the user before verification, per the system’s policy of never silently guessing at ambiguous input). The solver correctly found a counterexample at $a=b=0$ — the claim is false whenever $a=b$, since $(a-b)^2=0$ in that case, not strictly greater than zero. Breach’s automated proof autopsy then examined the system-generated proof steps and identified that the fourth step — “the claim asserts that this square is strictly greater than zero for all $a,b$” — implicitly relied on an unstated assumption: that $a$ and $b$ are distinct. The system stated this missing assumption explicitly (“the two integers are distinct, i.e., $a\ne b$”) and explained precisely how the discovered counterexample violates it (“Step 4 implicitly assumes the difference $a-b$ is non-zero, which would make its square strictly positive. The counterexample $a=b=0$ violates this hidden assumption, yielding a square of 0.”).

This example illustrates the intended behavior of the autopsy mechanism: rather than reporting only that a claim is false, the system localizes why it is false to a specific, previously implicit assumption in the reasoning, in language a user could directly use to correct the original claim (e.g., by adding the condition $a\ne b$). We view this diagnostic specificity — rather than the base true/false verdict, which the quantitative corpus of § 5 already evaluates — as the feature most clearly absent from the related systems discussed in § 2.

Limitations

We discuss limitations directly, in keeping with the system’s own design principle of stating uncertainty rather than concealing it.

Scope. Breach verifies bounded, mechanically decidable claims. It cannot and does not attempt to resolve open mathematical conjectures (e.g. the Collatz conjecture, the Riemann hypothesis, or infinite-dimensional continuous problems such as Navier–Stokes existence and smoothness) — these require open mathematical research, not mechanical search over a bounded or decidable space, and Breach’s own output explicitly states this rather than returning a misleading result. This is a deliberate scope boundary, not a current-version limitation expected to be lifted by further engineering.

Dependence on LLM translation correctness. Breach’s verification guarantee rests on the solver, but the solver only verifies the translated formalization, not the original informal claim directly. A systematically incorrect translation (for instance, one that inadvertently narrows or widens the intended domain of a claim) would produce a solver-correct answer to the wrong question. We partially mitigate this via the validation/retry mechanism described in § 5.2.1 and via always surfacing the translated formalization to the user, but we do not claim translation correctness is formally guaranteed.

Corpus scale and composition. Our validation corpus comprises 22 executable cases, predominantly drawn from miniF2F’s algebra and number-theory splits; this is sufficient to demonstrate the absence of confident-wrong verdicts across a real, externally-sourced sample, but is not a benchmark-scale evaluation and does not yet include coverage of geometry, the cube-and-conquer search path specifically, or the interactive challenge/autopsy mechanisms in quantitative form (§ 5 addresses the latter only qualitatively). Expanding corpus size and category breadth, including a dedicated quantitative evaluation of the challenge mechanism’s response quality, is left to future work.

No open proof construction. As discussed in § 1 and § 2, Breach does not generate proofs for true statements; it only falsifies or fails to falsify. A system combining Breach’s falsification-first prescreening with a proof-construction system — using Breach to cheaply rule out false candidate claims before expending proof-search effort on them — is a direction we consider promising but have not implemented or evaluated.

Conclusion

We presented Breach, a system for bounded mathematical claim falsification that uses a large language model exclusively for translation and natural-language diagnosis, delegating all verification decisions to deterministic solvers. Beyond the now well-established pattern of LLM-to-solver translation, we contribute an interactive, step-targeted challenge mechanism and an automated counterexample-to-assumption diagnosis procedure (“proof autopsy”), neither of which we find present in directly comparable prior systems. We validate Breach against a corpus curated from miniF2F, document a genuine instance of early-testing non-determinism transparently alongside its root cause and fix, and are explicit throughout about the boundaries of the system’s competence: it does not construct open-ended proofs, and it does not resolve genuinely open mathematical problems. We view Breach’s contribution as narrower and more honest than a general claim to “verify mathematics” — a tool that reliably tells a user what it checked, what it found, and precisely where its own certainty ends.

Acknowledgements

Breach was built with assistance from AI tools: Kimi CLI for implementation, testing, and debugging, and Claude for architecture planning, research positioning, and drafting of this paper. Every reported result in this paper was produced by executing the system’s own code (Z3, SymPy, and the validation corpus), not by taking a model’s self-report at face value.