[gnulinux]

I think you're onto something. When you formalize math you suddenly see how things summarized to one word or even implied implicitly can require pages of proof. But in this particular case, you're a little off. At least in conventional theorem proving (Coq, HOL, Agda) you mostly need 2 of those ("definition" and "equivalence") and for meta programmatic heuristic purposes (to help the solver) "constraint" too (except this has nothing to do with "proof proper").

Assignment isn't really needed for formal proofs since assignments usually requires a computational context that's not pure and most proofs are done tactics-like or functional style. I also can't see how "comparison" any different than "equivalence".

I would say the notion of "=" isn't the biggest difference here. I think what bugs people about "=" in automated proof systems is because (somehow?) our brain is really good at graph searching mathematical proofs and so typing equality proof in Coq, Agda, HOL is inherently too verbose.

Sorry to nitpick but this is an important topic as equality-reasoning is one of the harder parts of automated proof systems.