To Have Machines Make Math Proofs, Turn Them into a Puzzle (www.quantamagazine.org)

Carnegie Mellon researcher Marijn Heule argues that bridging classic satisfiability (SAT) solvers with large language models (LLMs) and formal proof checkers could produce tools capable of solving mathematical problems beyond human reach. Heule—who used SAT to settle long-standing puzzles like Schur Number 5 and Keller’s conjecture in dimension seven—says SAT’s brute-force, sound-search over Boolean constraints is a reliable backbone, while LLMs can provide the high-level decomposition and lemma generation that humans currently supply. The proposal is significant because it combines the soundness of symbolic automated reasoning with the generative, intuition-like abilities of LLMs, offering a path to machine-found proofs that are both new and verifiable. Technically, SAT frames problems as propositional formulas (true/false variables and constraints) and searches for satisfying assignments or certifies unsatisfiability; it also produces counterexamples that are small and informative. LLMs could automate the crucial encoding/representation step and suggest lemmas, while SAT solvers check those lemmas or return counterexamples to refine them; a formal system like Lean would then certify the final composition. Key challenges remain—guaranteeing correct encodings and taming LLM hallucinations—but Heule argues this human+LLM+SAT+formal-checker pipeline preserves mathematical trust even if the resulting computer proofs are long and opaque, keeping humans in the loop for creative guidance.