What is the motivation behind formalizing a piece of mathematics in a system like Mizar? I ask as someone interested in the process. I mean it's not like anyone is going to read those formal proofs. It's not like they are going to be useful for anything other than building more useless unreadable proofs, or are they? I would love to be wrong, but how does formalizing mathematics contribute to human understanding of mathematics?

  • $\begingroup$ Humans tend to make mistakes. I wouldn't be surprised that 99% of the proofs in scientific papers are wrong in details (and a significant fraction plain wrong). I agree that the verification of the proofs does little to understanding. The Holy Grail is a system that would allow mathematicians to express their intuitions and have a formal system help the validate. Just like CAS empower them. $\endgroup$ – Yves Daoust Feb 17 at 18:54
  • $\begingroup$ The same reason for using pocket calculators in addition to performing calculations by paper and pencil. $\endgroup$ – Mauro ALLEGRANZA Feb 17 at 19:04
  • $\begingroup$ Yes, but from what I've seen usually only basic (undergraduate) mathematics gets formalized. But there is not doubt about that being correct. $\endgroup$ – Adam Feb 17 at 19:20
  • $\begingroup$ How much mathematics has been formally verified? $\endgroup$ – Keith McClary Feb 18 at 2:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.