alt Hacker NewsAxiom 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.
Replies
What were the agents based on?
When two sources formalized the same object in incompatible ways, did the swarm mostly emit translation lemmas between them, or did someone pick a canonical definition and have downstream proofs rewritten to match? The second feels like where the "coherent whole" cost actually sits, and I'm curious how much of the 500-source effort was that reconciliation versus line-by-line translation.
As someone with a highly uneven and kinda basic maths background, I'd have thought that simplification of a proof, and pulling things into a coherent whole would be exactly what computers excel at, but everything I've seen (or heard) suggests that's not really the case. Are you able to explain why?