Agents Can’t Bluff a Kernel: Teaching AI to Prove Gauss in Five Proof Systems

The factorial function type-checked on the first try. It passed the termination checker. It compiled to C, ran natively, and printed an answer. The answer was wrong.

Not wrong the way LLM output is usually wrong — no hallucinated citation, no subtly plausible prose. Wrong the way only a machine can be wrong: fact(10) returned 986410 instead of 3628800, because the agent writing it had expressed the step as 1 + p * fact(p) instead of (1 + p) * fact(p). Every guarantee the language promised, it kept. Types: fine. Termination: fine. Intent: never checked, because intent is not a type.

That moment is why this post exists. We spent a day standing up an agent-driven lab around five proof and specification tools — Rocq (the artist formerly known as Coq), HOL4, Lean 4, Bend, and TLA+’s model checker TLC — and made AI agents learn each one from cold start, prove the same theorem everywhere, and fail honestly in writing. The experiment wasn’t “can agents write proofs.” They can, roughly, the way they can write anything. The experiment was: what happens to confident, fluent, wrong agent output when the reviewer is a proof kernel?

The answer, spoiler, is that it bounces. And the five ways it bounced taught us more about these tools than the five proofs that eventually landed.

The setup#

Five toolchains, one per agent, same brief: learn the tool by its actual documentation, write a hello-world proof, then prove one shared theorem — and record every false start verbatim, because the false starts are the transferable part.

The cast, taxonomized:

The shared theorem was Gauss’s summation identity, deliberately stated without division:

For all natural numbers n: 2 · (0 + 1 + ⋯ + n) = n · (n + 1)

As mathematics, this is nothing. Three lines on paper, known for centuries. We chose it precisely because it is the smallest theorem that still forces the full proving experience: define a recursive function, run an induction, then shuffle nonlinear arithmetic until both sides match. 1 + 1 = 2 only tests whether the tool launches. Gauss tests how it thinks.

The division-free form matters more than it looks: an equation in only + and × means no division lemmas, no truncation subtleties — and, crucially, it keeps the goal inside the territory of ring-arithmetic automation, which is where the most interesting refusals live.

Five tools, five ways to be told no#

Bend: the checker that made the wrong factorial possible#

Bend 2 is a young pure functional language with an unusual pitch: propositions are types, and a proof is just a terminating program of that type. There are no tactics, no proof search — the docs say so plainly. What happened with the factorial above is the canonical Bend experience: the checker verifies types and termination, not intent.

Bend’s answer to this is law — an equational specification you write separately, and prove with explicit rewrite steps. So for the Gauss theorem, the agent had to first grow its own arithmetic: the standard library ships zero arithmetic laws. Five hand-stated lemmas (add-zero, add-succ-right, associativity, commutativity, mul-succ-right) and ten explicit rewrites later, the proof stood at roughly 120 lines — the price of what ring gives Rocq users for one word.

Then came the adversarial control, which is the part worth remembering. We deliberately broke the summation function — dropped the + p from the recursive step — and re-ran. The broken program still compiled. Still terminated. Still ran (it computes 0 for everything). And the proof? Failed at its first rewrite, exit code 1, with the exact goal shape that diverged. The law binds. The wrong factorial of session one is exactly what laws are for.

What that looks like (lightly elided — each rewrite pattern quotes the entire goal, which is rather the point):

def sum_to(+n: Nat) -> Nat:
  match n:
    case 0n:
      0n
    case 1n+p:
      ((1n+p) + sum_to(p) : Nat)

# the law — intent, stated as a theorem to be discharged:
law gauss:
  for +n: Nat
  {Nat.mul(2n, sum_to(n)) == Nat.mul(n, Nat.add(n, 1n)) : Nat}

def gauss(n):
  match n:
    case 0n:
      {==}                      # reflexivity — both sides compute to 0n
    case 1n+p:
      # each %e quotes the whole goal, `_` marking the one subterm to
      # rewrite. The first, in full:
      %add0(Nat.add(p, sum_to(p))) :
        {Nat.add(1n, Nat.add(Nat.add(p, sum_to(p)), Nat.add(1n, _)))
         == Nat.add(1n, Nat.add(Nat.add(p, 1n),
              Nat.mul(p, Nat.add(1n, Nat.add(p, 1n))))) : Nat}
      %mul_succ_r(p, Nat.add(p, 1n)) : {...}
      %gauss(p) : {...}         # the induction hypothesis — used BACKWARDS
      ...                       # seven more rewrites, then {==}

HOL4: the error that exits zero#

HOL4 is an LCF-style prover — a tiny kernel is the only thing that can create theorems, and everything else is just SML code talking to it. Our agent’s Gauss proof eventually came down to three tactics, one of them a conversion aimed surgically at the left side of one equation, because both sides matched the distributivity pattern and the naive rewrite kept hitting the wrong one.

Theorem gauss:
  ∀n. 2 * sum_to n = n * (n + 1)
Proof
  Induct >> simp[sum_to_def] >>
  (* distribute the 2 across (SUC n + sum_to n) — left side of the
     equation ONLY, because both sides match the pattern *)
  CONV_TAC (RATOR_CONV (RAND_CONV (ONCE_REWRITE_CONV [LEFT_ADD_DISTRIB]))) >>
  gvs [ADD1, GSYM RIGHT_ADD_DISTRIB]
QED

The instructive failure came earlier: the classic idiom for nonlinear goals — load up the simplifier with associativity and commutativity lemmas — made the session hang. No error. No output. Just silence, forever. Bisection with timeouts isolated the culprit: a commutativity rewrite used as a plain simplification rule feeds every permuted term back into the rewriter. A diverging proof search looks exactly like a slow one.

And the trap underneath the trap: a piped HOL session exits 0 even after a static error kills the rest of your input. The process status is a lie; the transcript is the truth. Any automation that trusts exit codes here will confidently report success on garbage.

Rocq: the simplifier that simplified too much#

Rocq gave us the purest example of a tool refusing a plausible move. After induction, the natural instinct — simpl to unfold the recursive definition — compiles the goal right past the shape the induction hypothesis needs. rewrite IHn then fails with “Found no subterm matching,” and nothing in that message hints that the problem happened three tactics earlier. The fix is cbn [sum_to]: unfold exactly one function, touch nothing else. “Simplify less, but on purpose” is a proof-engineering lesson that generalizes far past Peano arithmetic.

Theorem gauss : forall n, 2 * sum_to n = n * (n + 1).
Proof. induction n.
  - reflexivity.                          (* base: both sides convert to 0 *)
  - cbn [sum_to].                         (* unfold ONLY sum_to *)
    rewrite Nat.mul_add_distr_l, IHn.     (* expose 2 * sum_to n, then use it *)
    rewrite !Nat.mul_add_distr_l, !Nat.mul_1_r.
    rewrite Nat.mul_succ_l, Nat.mul_1_l, Nat.mul_succ_l, Nat.mul_succ_r.
    rewrite Nat.add_comm, Nat.add_assoc. reflexivity. Qed.

Rocq also gave the day’s genuine surprise. We expected the nonlinear step — the (n+1)(n+2) product — to defeat lia, the linear arithmetic tactic. It doesn’t: micromega normalizes products into monomials first, so the goal becomes linear in {sum, n², n, 1} and one tactic closes the whole theorem. Our prediction was wrong in public and the kernel corrected us the same way it corrects agents. Fitting.

Theorem gauss_lia : forall n, 2 * sum_to n = n * (n + 1).
Proof. induction n; simpl; lia. Qed.

Lean: the arithmetic tactic that sees atoms, not algebra#

Lean’s omega is superb and honest about its limits, but the limits are architectural: it abstracts products of sums as opaque atoms. After the induction, the agent’s goal had n * (n + 1) on one side and (n + 1) * ((n + 1) + 1) on the other — same algebra, different atoms, and omega quite reasonably declined, dropping the nonlinear hypothesis entirely. The proof that works distributes exactly one side of the equation by hand, so both sides finally share an atom, and then omega finishes.

theorem gauss : ∀ n, 2 * sum_to n = n * (n + 1) := by
  intro n
  induction n with
  | zero => rfl
  | succ n ih =>
    -- distribute 2 over the sum, use the IH, then distribute ONLY the
    -- right-hand side (Nat.mul_add n (n+1) 1, instantiated explicitly so
    -- the rewriter cannot touch the LHS) — now n*(n+1) is a shared atom
    rw [sum_to, Nat.mul_add, ih, Nat.add_mul,
        Nat.mul_add n (n + 1) 1, Nat.mul_one, Nat.one_mul]
    omega

With mathlib attached, the same induction step closes with a bare ring. The gap between core Lean and mathlib is the gap between “understand your atoms” and “don’t worry about it” — and both states are worth experiencing once.

The audit trail, for the record: #print axioms gauss reports [propext, Quot.sound]. The proof depends on nothing else — not even excluded middle. That one command is the kind of instrument panel agents should be taught to read.

TLA+ / TLC: no proof, and proud of it#

The fifth tool isn’t a prover at all. The tla2tools jar contains a parser, a model checker, a simulator, and a PlusCal translator — and zero proof machinery (we counted the classes; the proof assistant TLAPS is a separate product entirely). TLC’s relationship to the Gauss statement is refreshingly honest: it evaluated 2·Σ and n(n+1) for every n up to 200 and said, in its exact words, “Model checking completed. No error has been found.”

EXTENDS Integers
CONSTANT N                          \* the bound we fund
VARIABLE dummy                      \* TLC rejects a variable-free Init
sum[n \in 0..N] == IF n = 0 THEN 0 ELSE n + sum[n - 1]
GaussOK == \A n \in 0..N : 2 * sum[n] = n * (n + 1)
Init == dummy = TRUE
Next == dummy' = dummy /\ FALSE     \* never enabled, but not a constant
====

No error has been found — past perfect, bounded, no promises about n = 201. And when we flipped the property to a false one, TLC produced a counterexample rather than a failed proof search. Except when it didn’t: a variable-free false invariant gets constant-folded before the state machine runs, and fails with an error but no counterexample trace. Same tool, same theorem, two entirely different failure textures depending on whether a state variable appears in your predicate. That’s the kind of edge an agent learns by hitting it.

The mirror in the middle#

Halfway through, the lab produced its most transferable single fact, and it’s almost embarrassingly small: check which argument your + recurses on.

In Rocq and Bend, addition is defined by recursion on the first argument — so 0 + n computes for free, while n + 0 is a stuck term that needs induction. In Lean, Nat.add recurses on the second argument — so n + 0 = n is true by rfl alone, and 0 + n = n is the one that needs work. The same trivial statement, on opposite sides of the reflexivity line, in tools whose surface syntax barely differs.

Every agent hit this wall in session one, from opposite directions, and no amount of fluent prose about “obvious identities” moves the wall. The kernel does not care what is obvious.

The price list#

For the identical theorem, the final cost sheet:

Read as a tool-selection guide: automation-rich tactic provers for algebra-heavy goals; term-level checkers when you want the proof itself to be auditable; model checkers when you want counterexamples fast and the universal quantifier is not yet your problem.

Calibration, because someone will ask#

None of this is deep mathematics. Gauss is the “hello world+” of induction, and our proofs are toy-sized. For scale: Feit–Thompson in Coq took a team roughly six years and about 170,000 lines; the Liquid Tensor Experiment in Lean took a community about eighteen months; verified kernels and compilers are multi-year programs. We stress-tested toolchains and agents, not mathematics. The toy size is the point — at this scale, every failure is legible, and legible failures are what you want when teaching (or being) a learner.

The scorecard: how each tool actually performed#

With the failure stories told, here is the verdict view. Session time is agent wall-clock including write-ups — an honest proxy for friction, not a benchmark:

Read as verdicts: Rocq is the fullest package — the same theorem at every altitude from ten legible rewrites to a one-line lia, with the best library-discovery loop once you learn shape-based Search. Lean is the smoothest ride with the best error messages and a real instrument panel (#print axioms); core-only is the most educational struggle, mathlib is the difference between homework and one word. HOL4 has the airtight LCF kernel and the worst ergonomics — it rewards exactly the precision it demands and punishes hopeful automation; not the tool to learn on, arguably the one to end up on. Bend costs the most per theorem by far (the standard library ships zero arithmetic laws) but lost the least trust: instant checks, surgical errors, and the one feature nobody else showed — a spec whose binding we verified by sabotage. TLC reaches a verdict fastest of all five and is alone in handing you counterexamples; it just isn’t proving anything beyond the bound you fund.

The one-line ranking, if you’re taking notes:

• Learn to prove on: Rocq or Lean
• Want the proof to be readable code: HOL4 or Bend
• Want to know that it’s false, fast: TLC
• Best automation-per-minute: Rocq lia
• Most honest failure messages: Bend, then Lean
• Most likely to silently waste your afternoon: HOL4 (divergence)

And the meta-result: agent time correlated almost perfectly with available automation — the less a tool decides for you, the more the session costs. That’s either a bug or the entire point, depending on what you showed up to learn.

How the lab itself worked#

Method disclosure, since the meta-story is half the claim:

• Each tool got a dedicated agent with the same brief: read the real docs, write hello-world, prove the theorem, keep every error message verbatim. Five independent transcripts, no shared context.
• Nothing entered the record on an agent’s word. The orchestrator re-ran every winning proof from a clean slate — deleted artifacts, full rebuilds, fresh sessions, kernel-level rechecks (Rocq’s rocq check re-verifies a compiled library with the kernel alone; HOL’s stored theorem printed from a fresh session; Lean’s axiom audit) before anything was committed.
• Every tool got an adversarial control: a deliberately wrong implementation or false property, verified to fail in a visible way. A check that can’t fail is a check you haven’t run.
• Everything learned went into a knowledge graph for future sessions, so the next agent (or human) starts from the trap map, not from zero.

The discipline is the finding, really. Agents generate candidates at a rate no human matches, and most candidates are wrong in ways that look right. Ordinary review — tests, spot checks, vibes — filters some of that. Proof kernels filter all of it, at the exact boundary where the claim becomes formal. The failure modes we catalogued (silent divergence, lying exit codes, folded invariants, plausible rewrites on the wrong side of an equation) are all real, and all survivable — once you know they’re the terrain instead of bugs in your approach.

What’s next#

The lab continues: richer theorems where the tools genuinely diverge (irrationality of √2 wants different machinery than Gauss), TLAPS to give TLA+ a proof side, and Bend’s law workflow exercised on something that isn’t arithmetic. The trap map grows. The kernels don’t budge.

That’s the comfort in it. In a year of watching language models produce ever-more-confident output, the proof kernel remains the one reviewer whose confidence is exactly as large as its proof — and whose mind cannot be changed by anything except a term that checks.