Axiom MTS here. What you describe is pretty close to how we formalised this proof, which is scattered across more than 500 articles and books: a swarm of agents was tasked with going through all these sources.
One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways.
One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways.