Interesting. What about machine proof checking? Why don’t mathematicians publish all results in a formal notation (in addition to the human-oriented one) that allows all proofs to be checked, and entered into an Internet repository available to automated proof assistants?
For the same reason not all software is written in Coq/Agda/other proof systems: it would be incredibly expensive, slow, and demand very rare skills.
Interesting. What about machine proof checking? Why don’t mathematicians publish all results in a formal notation (in addition to the human-oriented one) that allows all proofs to be checked, and entered into an Internet repository available to automated proof assistants?
For the same reason not all software is written in Coq/Agda/other proof systems: it would be incredibly expensive, slow, and demand very rare skills.
Because it takes a lot of extra time and work to formalize a proof to the level where it can be automatically checked.