Graffiti3Loop: Generating and Resolving Formal Machine-Generated Graph Conjectures in a Loop

We introduce Graffiti3Loop, the first loop that autonomously generates formal graph-theoretic conjectures in Lean4 and attempts to solve them. The conjectures are machine-generated byGraffiti3Loop from finite invariant tables, automatically translated into typed Lean4/mathlib statements, and checked (where Lean4 versions allow) with Lean-FRO Comparator so that a submitted proof must solve the intended formal challenge rather than merely compile. We use a batch of 330 selected conjectures to ground this loop in concrete outputs, which we call Graffiti3Bench-330. In a zero-tool baseline with three open-weight Lean prover checkpoints, no tested output was accepted; we therefore report a failure-mode analysis covering moved or missing Lean APIs, unsolved goals, missing answer blocks, impermissible proof shortcuts, and malformed proof fragments. By contrast, a tool-using, human-guided agentic triage that ran through Graffiti3Bench-330 produced $42$ Lean-checked labels: $17$ proofs of likely new true items and $25$ explicit disproofs. A further $85$ items have computational counterexamples, while $203$ remain likely true after bounded counterexample search. The benchmark part of this loop is intended to measure AI-for-mathematics systems on machine-originated conjectures that sit closer to mathematical discovery workflows than static exercise corpora, including proof, refutation, and hypothesis-repair settings, paving the way for a new engineering-driven approach to mathematics.