This is true of literally any proof of sufficient complexity, human-authored or otherwise.

It takes time to convey the core ideas. It takes time for other mathematicians to come up to speed on the new techniques and approaches or the novel combinations of existing ones.

The actual experts in this field have asked for the argument to be explained to them, and are now at the point where they believe this is plausible. Another person in this thread has produced a Lean proof and presumably is not trying to pull a fast one on us by exploiting a bug in the solver.

TL;DR chill bro.