Sudoku Search Lab

Sudoku Search Lab needed to be three things at once: a demonstration, an explanation and a test. It is also yet another side quest (OpenAI has sworn off those; I have not).
It started with P vs NP. I remember reading about the Millennium Prize Problems and dreaming of solving one. Keith Devlin’s The Millennium Problems (2002) predicted that P vs NP would fall to an “amateur” (someone without a mathematics PhD) (NPR, 2003), because the problem is easy to explain and understand, yet hard to solve. That is more or less what the problem is about: some answers are hard to find (sometimes impossibly so) but easy to check. Think of the test in Inception: you have two minutes to design a maze that takes one minute to solve.
My fourth year of Computer Science was the first time I took Artificial Intelligence, and it is still my favourite course of all time. I never took computers in high school. By 12, though, I was sneaking my older brother’s senior homework and solving it easily. University was the first time I was classically educated: Computer Science, plus the adjacent essentials (physics, logic, discrete and continuous mathematics, statistics). Of all of it, nothing fascinated me more than AI, even if we mostly focused on machine learning.
My favourite part was writing programs in LISP and Prolog. It was a major paradigm shift. Instead of writing the solution as an algorithm, you wrote programs that could find the solution; the logic turned back on itself. I used it to build a (not-so-good) Sudoku solver. Sudoku is one of my unplugged activities (got to keep the logic sharp!).
Years later I learned that Sudoku, generalized to larger grids, is NP-complete. Flashback.
So here it is. You can have it solve a range of difficulty levels and try a few different search strategies. You can step through a puzzle one move at a time, or phase by phase. On hard puzzles you can watch it struggle and backtrack, which is nothing like the way a person solves one. You can also see its decision tree in several forms (signal, wave, graph). Fascinating stuff. A short background on P vs NP rounds it out; that is the demonstration and the explanation.
The test came later. Could I find an approach to P vs NP and apply it here? My hunch is a centaur: a human teaching an agent skills, so that something non-deterministic (the LLM) helps write something deterministic (the solver). Fittingly, the N in NP stands for nondeterministic. However, a faster solver would not settle anything on its own. Settling P vs NP takes a proof that every NP-complete problem, at every size, can be solved in polynomial time (the question Stephen Cook posed in 1971, from the University of Toronto); a clever 9×9 solver demonstrates, but it doesn’t prove. Does the hunch need a human in the loop, and how would I even test that? Can a human and a computer together beat a computer alone at Sudoku? That question leads straight back to the Latent Mirror thesis.