A Closed-Loop System of 3 Mathematical Agents: Conjecturer, Refuter, and Prover

We present a closed-loop autonomous system for mathematical discovery. In this paper, “autonomous” refers to execution-level autonomy: after initialization, one command runs conjecture generation, counterexample search, formal proving, outcome reconciliation, and the next generation without human intervention between stages. The system generates conjectures in the form of linear inequalities, searches for counterexamples, and sends surviving statements to a Lean 4 prover with a zero-sorry policy. The concrete setting is polyhedral combinatorics. The system separates proposal, verification, and learning. Outcome-dependent signals may influence the conjecture generator, but do not modify the counterexample validator, exhaustive search procedure, or proof-acceptance gates. Accepted counterexamples contain explicit witness graphs and pass five validation checks; accepted proofs are compiling Lean artifacts whose root theorems match the generated statements. The system also separates arithmetic feasibility from geometric realizability. In the current repository version, the campaign records 204 witness-verified refutations, four end-to-end machine-proved conjectures (C104, C124, C201, and C215), and three open conjectures (C193, C195, and C198). The main contribution is an artifact-producing autonomous workflow that preserves refutations, proofs, and unresolved cases as reusable computational or formal objects.