Solving Semidecidable Problems in Group Theory

Decision problems about infinite groups are typically undecidable, but many are semidecidable if given an oracle for the word problem. One such problem is whether a group is a counterexample to the Kaplansky unit conjecture for group rings, a conjecture that was open for 80 years. In this talk from the recent Simons Institute and SLMath joint workshop, AI for Mathematics and Theoretical Computer Science, Giles Gardam (University of Bonn) presents the mathematical context and content of the unit conjecture, and explains how viewing the problem as an instance of the Boolean satisfiability problem (SAT) and applying SAT solvers show that it is not just solvable in theory but also in practice.