You might as well have written that mathematicians should stop doing mathematics. If every mathematician were to work full time on formalizing theorems in proof

You might as well have written that mathematicians should stop doing mathematics. If every mathematician were to work full time on formalizing theorems in proof assistants, then no living mathematician would ever do original research again -- there is simply too much that would need to be translated to software. And to what end? It's not as if people suspect that the foundations of mathematics are on the verge of toppling. > Code is easy to share, easy to collaborate on [...] collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff Here's an experiment anyone can try at home: pick a random article from the mathematics arxiv [1]. Now rewrite the main theorem from that paper in Lean [2]. Did you find this task "easy"? Would you go out of your way to finish the "tedious" stuff? > even horrible code is far better at documenting what it does than what you are describing The "documentation" is provided by talking to other researchers in the field. If you don't understand some portion of a proof, you talk to someone about it. That is a far more efficient use of time than writing code for things that are (relatively) obviously true. (No shade on anyone who wants to write proofs in Lean, though.) --- [1] https://arxiv.org/list/math/new https://arxiv.org/list/math/new [2] https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html https://lean-lang.org/theorem_proving_in_lean4/dependent_typ...