In theory, yes, but in practice proof assistants are only just starting to become practically useful for research-level mathematics. Validation/verification would likely require an enormous amount of proof engineering to build up the theorems required to verify a proof of this complexity. See the Liquid Tensor Experiment postmortem [1] for the results of a similar undertaking.

[1]: https://leanprover-community.github.io/blog/posts/lte-final/