1. 9
  1.  

  2. 2

    This is probably my favorite way to use proofs: take an idea from a real world problem, abstract it so it’s expressible as simple definitions and theorems, and see if the idea is true.

    And as was shown here, this can often be done in a proof assistant with just a few lines of script / tactics. That QED is a wonderful feeling.