Marijn Heule has spent a decade wrestling with the stubborn mechanics of computer-aided mathematics. As an associate professor of computer science at Carnegie Mellon University, he knows the old frustrations firsthand. Reformulating a conjecture so a solver could attack it demanded specialist skill. That bottleneck kept powerful tools beyond the reach of most working mathematicians. LLMs have begun to change the equation. Heule’s recent piece in…