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?
A few unrelated examples:
Some books assume 0 is Natural but other start from 1.
In some books all Rings https://en.wikipedia.org/wiki/Ring_(mathematics) have a multiplicative identity. Almost all books assume Algebras have an identity, but there may be weird cases.
Some books say in the first page that they will assume all groups are Abelian/Commutative, and not repeat the assumption in each page.
There are like 8 conventions to define the Fourier Transform. All are equivalent, but each one add different constants here and there. Beware to combine formulas from different books.
I guess it's easier for the computer to track the details and remember to translate the names in each book article to a consistent set of definitions.
Proof and program are twins. Formalized theorems can be incompatible for exactly the same reasons that programming APIs can be incompatible.