Comment by petesergeant
5 hours ago
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?
Proof and program are twins. Formalized theorems can be incompatible for exactly the same reasons that programming APIs can be incompatible.