The Curry–Howard isomorphism states that computer programs are directly equivalent to these mathematical constructs, which can be automated using the languages Lean or Rocq (“rock”). For 10 points each:

<Other Science>