Genuinely interested in being educated here: If Gurobi's integer programming solver didn't find a solution better than 218, is that a guarantee that there exists no solution better than 218? Is it equivalent to a mathematical proof?

(Let's assume, for the sake of argument, that there's no bugs in Gurobi's solver and no bugs in the author's implementation of the problem for Gurobi to solve.)

I guess I'm basically asking whether it's possible that Gurobi got trapped in a local maximum, or whether this can be considered a definitive universal solution.

In addition to the value of the best integer solution found so far, Gurobi also provides a bound on the value of the best possible solution, computed using the linear relaxation of the problem, cutting planes and other techniques. So, assuming there are no bugs in the solver, this is truly the optimal solution.

I'm not sure about Gurobi or how the author used it in this case. But in general, yes: these combinatorial solvers construct proof trees showing that, no matter how you assign the variables, you can't find a better solution. In simpler cases you can literally inspect the proof tree and check how it's reached a contradiction. I imagine the proof tree from this article would be an obscenely large object, but in principle you could inspect it here too.

In theory, it's not proof. In practice, it is.