CRAFT: Counterexample-guided Repair And Falsification of Theorems in ML and Optimization

AI systems are increasingly used as research assistants, and mathematical reasoning is a central capability for research across mathematics, engineering, AI, and the sciences. Recent LLMs and reasoning-oriented systems have made rapid progress on mathematical problem solving, but plausible natural-language reasoning is not reliable verification. Models can produce confident explanations for false claims, and checking those explanations by hand may simply move the bottleneck from generation to verification. We present \textbf{CRAFT} (\textbf{C}ounterexample-guided \textbf{R}epair \textbf{A}nd \textbf{F}alsification of \textbf{T}heorems), a counterexample-first workflow for mathematical claims that admit executable falsification. CRAFT first asks an LLM to analyze a natural-language claim and produce a structured true/false/uncertain judgment with a verbal rationale. A verifier then searches for concrete counterexamples: found counterexamples are fed back to expose errors and support repair, while calibrated no-counterexample signals can prompt reconsideration of false alarms. Repaired statements are re-checked through the same executable interface. On a 50-claim benchmark spanning 25 ML/optimization families, verifier feedback improves or preserves accuracy across seven models. For \texttt{qwen2.5-7b-instruct}, accuracy improves from 78\% to 94\%. Search quality determines verifier reliability, verifier feedback corrects errors in the round-1 LLM-only baseline, and all 25 canonical repair targets pass re-checking.