1. 14
  1.  

  2. 2

    I like how Metamath is fast at verifying proofs. It is a refreshing change after having to wait for type-driven solvers to do their type-checking.