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?
replyProof and program are twins. Formalized theorems can be incompatible for exactly the same reasons that programming APIs can be incompatible.
replyWhat were the agents based on?
replyWhen 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.
reply[flagged]
replyProducing a formalized proof from a non-formalized proof in a paper or book should not be considered a violation of copyright.
replyIndeed; one cannot copyright mathematical ideas, only their specific expressions. And the formalization is a different expression.
reply