It's nice to know that they didn't miss anything. The natural language proof is 10,000 pages and they have missed groups in the past.

The proof was of such complexity and length there were lingering doubts. This dispels them.

More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.