I absolutely think that with the rise of LLM generated theorems we need mechanization more than ever, yeah. But I felt that was already pretty important for human proofs, too, and people are just more amenable to the idea now that it doesn't take such heroic effort to formalize things.

As far as whether something like Lean could evaluate this proof: sure, if it were mechanized rigorously. But the amount of work that takes to do varies with both subject and complexity of result. In this case, from what other people are saying, the infrastructure for doing graph theory proofs like this isn't as built up as it is for some other areas of mathematics, so it might take a while.