The point is not to prove that 1+1=2. The point is to construct mathematics (all of mathematics) directly from the axioms using a formal language. The objective of 1+1=2 is not interesting, but the result is a rigorous foundation of mathematics using formal languages.
The upshot is twofold: (1) we have a rigorous foundation of mathematics in formal logic which CAN be used to prove nontrivial statements, as in the application of model theory to mathematics, and (2) we can now build proof assistants that allow us to use computers to better understand proofs.
Both applications of formal reasoning are equally interesting and have wide ramifications in mathematics.
The upshot is twofold: (1) we have a rigorous foundation of mathematics in formal logic which CAN be used to prove nontrivial statements, as in the application of model theory to mathematics, and (2) we can now build proof assistants that allow us to use computers to better understand proofs.
Both applications of formal reasoning are equally interesting and have wide ramifications in mathematics.