A formal proof in the sense of Hilbert's formalist program or one produced by an automated theorem prover is very different from the proofs presented in journal

A formal proof in the sense of Hilbert's formalist program or one produced by an automated theorem prover is very different from the proofs presented in journals. The latter are full of "it is easy to see that [...]", after which they proceed to state something which is not obvious to 99% of the population--nor to any computer, for that matter. I submit that the Principia did not change the status of 1+1=2 at all, but only used it to illustrate the correctness of its formalization of arithmetic. It was more like a soundness check: we _know_ that 1+1=2, so if it can be proved in our system it's a good thing.