I too remember reading about the four color map solution. Perhaps I'm thinking too much within my own skillset which is programming rather than mathematics where I'm much weaker. But I thought I understood the difference between a mathematical proof and a mechanical one. The conjecture here may be expressed mathematically and the mechanical proof sound, but in order to qualify as a mathematical description it shouldn't really include every instance of the object it wishes describe (ie it would be nice if it was much smaller). That's the whole point of maths - it’s a shortcut to the truth. We/They are lucky the Sudoku problem is finite otherwise a mechanical proof would always remain out of reach, in contrast to, say, the Pythagorean theorem where we can't examine every triangle. I think they have used some very attractive maths/logic to reduce the search space and get to the proof in a reasonable time but I wanted to make a layman distinction in this area of proof.
Have a great Christmas