Comment by jovas

Yes, I'm a mathematician.

But not an expert on this.

While I don't know the specifics, and someone more "in-the-field" than me would recognize all the "named" theorems etc

I am aware that there have been minor issues that have come up with the formalization specifically, and that previous proofs for lower values of n were always needed.

Though it used to be n=5 and lower needed to be checked.