> arrival of a machine that helps me dig faster This is usually wrong for the current SotA of ITPs. One important difference between verified programs (that t

> arrival of a machine that helps me dig faster This is usually wrong for the current SotA of ITPs. One important difference between verified programs (that the article mentions is useful) and mathematical results is that the former usually involves properties that are very complicated to state with many moving parts, but are usually straightforward to prove. On the other hand, mathematical results usually have a straightforward central concept, and the complicated details (if there are) can be altered to slightly change the result. To the mathematician, these complicated details are understood to be nonessential to the result and can be omitted, or reduced to a a comment or reference. And if the theorem is wrong, it can usually be salvaged. But with provers, you are forced to get bogged down in the details. The analogy to mining machines is wrong; the appropriate comparison is something more like writing in Python vs. writing in assembly. Writing in assembly you have a better guarantee that the computer is behaving exactly as you told it to. But it's less portable (e.g. you must decide to encode tuples primarily as a product, or as a finite sequence, one of many nonessential decisions that are important to a prover), just as asm is less portable than a python program. You have to get bogged down in details that you can make errors in that you don't in Python; (respectively, informal proof). It's harder for peers to understand the thrust of what is happening. etc.