Marijn Heule turns mathematical statements into something like Sudoku puzzles, then has computers go to work on them. His proofs have been called “disgusting,” but they go beyond what any human can do.

The mathematical conundrums that Marijn Heule has helped crack in the last decade sound like code names lifted from a sci-fi spy novel: the empty hexagon. Schur Number 5. Keller’s conjecture, dimension seven. In reality, they are (or, more accurately, were) some of the most stubborn problems in geometry and combinatorics, defying solution for 90 years or more. Heule used a computational Swiss Army knife called satisfiability, or SAT, to whittle them into submission. Now, as a member of Carnegie Mellon University’s Institute for Computer-Aided Reasoning in Mathematics, he believes that SAT can be joined with large language models (LLMs) to create tools powerful enough to tame even harder problems in pure math.

“LLMs have won medals in the International Mathematical Olympiad, but these are all problems that humans can also solve,” Heule said. “I really want to see AI solve the first problem that humans cannot. And the cool thing about SAT is that it already has been shown that it was able to solve several problems for which there is no human proof.”

SAT is actually one of the foundations of artificial intelligence itself, although not the kind of AI that makes headlines by mimicking fluent conversation or spooking researchers with supposedly “evil” thoughts. Instead, SAT belongs to the tradition of symbolic artificial intelligence (also known as GOFAI, or “good old-fashioned AI”), which uses hard-coded rules — not the inscrutable interactions within a deep neural network — to produce results. In fact, SAT is about as simple as AI gets, conceptually speaking: It relies on statements that can have only two possible values, true or false, linked together in ironclad chains of logic. If problems can be ground down into these logical “atoms,” computer programs called SAT solvers can often build airtight proofs about them — a process called, appropriately, “automated reasoning.” Those proofs might be long, sometimes too long for humans to ever parse ourselves. But they are sound.

...read more at quantamagazine.org