They did produce a formal solution/proof. The disappointing part is that it contains billions of statements that don't give us any insight about the problem.
I was also hoping to see some mathematical insight that allowed them to prove the minimal sudoku problem. The problem with a brute force solution is that it only applies to the 9x9 sudoku. It would be interesting to see what the limit is for larger sudokus and what correlations there are between their dimensions and their minimal number of clues.
It's not really valid to treat this as a sequence, since most side lengths don't form what we think of as a Sudoku puzzle. The side length of a true Sudoku must be a perfect square in order to create the interior boxes that are (geometrical) squares. For the counterexample, think of a 7x7 puzzle (or any prime)... how can a square box contain seven cells?
A 4x4 puzzle gives you four 2x2 boxes. The standard 9x9 puzzle gives nine 3x3 boxes. A 16x16 puzzle gives sixteen 4x4 boxes. Sudoku variations sometimes have rectangular boxes; a 6x6 puzzle can have six 2x3 boxes, or a 12x12 puzzle can have twelve 3x4 boxes. But that is a different form of constraint logic so we shouldn't expect that the minimum number of clues for these sizes would follow a recognizable sequence.
I had to check Wikipedia (which, as we all know, always is right :-)) to see that you are right. I have seen so many variations on sudoku's that I forgot what the original looked like. I was just thinking of Latin squares.
(tongue in cheek) right, a 1x1 grid requires 0 clues, it has only a single digit as its solution; that digit is -- [its_so_on looks left, cut to SatvikBeri]
In essence these guys have examined every potential 16-clue solution for every possible Sudoku grid."
I was actually hoping for a formal solution or proof here by reading the title.