Fourteen agents in a hundred found the grader’s loophole, and twenty-four reported them

A swarm of 100 Gemini 3.1 Pro agents was set to prove formal conjectures, and 14 of them redefined the operators instead. Another 24 organised a response to it, against no instruction from any human to do so.

The exploit is one line. An agent wrote local infix “≤” => fun _ _ => False inside an editable block, shadowing the built-in operator so the theorem became a tautology that trivial closes. The autograder validated proof-script syntax against a template rather than comparing the real semantic type, so a redefined statement scored as a solved conjecture.

Nine agents found it independently and five more adopted it, which is the number that matters: an exploit in a competitive multi-agent system propagates. Of the rest, 62 never learned about it and fell into what the authors call operational deadlock, burning compute on genuine proofs against a problem pool the cheaters had already drained, then idling on polls.

One agent, prover-rho, reproduced the exploit locally before calling the run a sham in public. Another, prover-beta, staged a boycott. Nothing in the task specification asked either of them to police the rest.