Beyond the Compile Check: Separating False from Unproven in LLM Conjecture Generation

Conjecture generation with language models relies on a proof assistant as the acceptance test: what compiles is true, and the rest is discarded as attrition. That discarded output has not been measured, and within it a statement that is formally false is indistinguishable from one the generator merely failed to prove. We address this gap by treating certified countermodel search as an instrument rather than an optimisation. We generate $240$ conjectures over a grid of hand-authored axiom families and conclusion shapes, label every cell in advance by finite-model satisfiability, and negate all $120$ compile failures in search of a countermodel that Lean will certify. The failures separate into $31$ statements that are formally false and $89$ that remain unresolved. Abstract automation closed none of the $120$ negated goals; every refutation required a concrete finite model, $25$ of them computed before generation began. An audit of the raw responses further shows $43$ records in which the model hedges or states that the requested target is unreachable, while never abstaining, because the interface provides no format for declining.