Post AfeoVEJhL7885cXqpU by soaproot@sfba.social
 (DIR) More posts by soaproot@sfba.social
 (DIR) Post #AfeoVEJhL7885cXqpU by soaproot@sfba.social
       0 likes, 0 repeats
       
       Why would you prove theorems in a computer-checkable format? Without one, if you publish a proof it takes highly skilled experts a year to figure out whether your proof is correct (if you are credible enough that they'll bother). With one, the computer is checking each step of the proof and the humans only need to compare what you prove with what you claim to have proved. I prove #constructiveMathematics at https://us.metamath.org/ileuni