3 ms·

Is this something a proof assistant could be used to help validate?

• bmc7505 4y ago
  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/ https://leanprover-community.github.io/blog/posts/lte-final/