Mathematical papers will not come with a formal proof until formal proof systems "auto-prove" button is strong enough to do everything for them and it can come

Mathematical papers will not come with a formal proof until formal proof systems "auto-prove" button is strong enough to do everything for them and it can come as an afterthought that takes 5 minutes. Formal proofs do nothing to help understand the mathematics, all they do is help to check for errors in logic -- have you ever read a formal proof? They are leagues more obtuse and difficult to understand than any piece of mathematics from any field. A program is technically truth-value equivalent to doing a proof, but the resulting document/piece of text are MILES apart. The proof is an explanation in plain language to others who understand the topic why something is true. The formal proof is a sequence of opaque inference rules that the computer promises is equivalent to a real proof. It's the difference between understanding a formula and plugging it into your calculator. The calculator is more likely to compute correctly, but it gives you no help when it comes to actually understanding mathematics. Mathematicians as a community completely reject the notion of using formal proofs (while sometimes begrudgingly accepting they may be useful to check our work) because they completely miss the point of what we are actually doing.