Lean Disprove: Certified Counterexample Search for AI-Assisted Formal Mathematics

LLM-driven formal mathematics has focused mainly on proving true statements; the complementary task of disproving false ones (finding a counterexample the proof assistant can certify) has had little dedicated tool support. We present /disprove, an interactive command for coding agents in the open-source lean4-skills package. Given a Lean goal, the command runs a bounded six-phase cycle to perform certified counterexample search: it profiles the target, consults prior knowledge, selects a disproof method from a registry (including decision procedures, finite enumeration, random sampling, and external scripts such as SAT/SMT queries), searches for a witness, and assembles a shape-specific negation term. It reports REFUTED only when Lean accepts the refutation, and otherwise reports WITNESS-UNCERTIFIED, when a candidate witness was found but could not be certified, or INCONCLUSIVE, when no candidate was found. External witnesses are never trusted directly, but must be lifted into Lean and checked by the kernel. We demonstrate on a pilot benchmark that it certifies counterexamples a bare decision procedure cannot reach, while never refuting a true statement.