To Have Machines Make Math Proofs, Turn Them Into a Puzzle | Quanta Magazine
www.quantamagazine.org
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…

Source

From Quanta Magazine via this RSS feed