3 ms·

Soo... Unit testing / CI for math proofs? If it can be done in software, great.

• std_throwaway 7y ago
  To my knowledge the hard part is writing the input for the software. While in text you have a bit of leeway to glance over some details, with the computer program you must, indeed, write every last relevant detail down and you must get it right. This is very heavy work.
  • ukj 7y ago
    But it's once-off work. Thereafter the computers can take over.
• jeff_friesen 7y ago
  I was thinking it's a lot like property-based testing
• jetzzz 7y ago
  It's actually type checking. Per the Curry–Howard correspondence, proof checking is equivalent to type checking, just for much more sophisticated type system than in an ordinary programming language.