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?

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.

[flagged]

The really interesting aspect of this, IMHO, is discovering what theorem formulations combine together well as a whole. It's much akin to a software architecture problem.

Metamath has done quite a bit or primary research into this. Theorems often have a slightly non-standard, but more general form.

One can ask things like, "what is the equivalent of functional programming?" Or, "is there global state?" It's a perspective on reverse mathematics.

> Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.

Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).