> Occasionally we mathematicians find that we need a new tactic—for example proving that (a+b)^3=a^3+3a^2b+3ab^2+b^3 just from the axioms of a ring is surprisin

> Occasionally we mathematicians find that we need a new tactic—for example proving that (a+b)^3=a^3+3a^2b+3ab^2+b^3 just from the axioms of a ring is surprisingly difficult! Perhaps because what you need there is not just a ring, but a commutative ring :P Jokes aside, that was an excellent article and introduction to interactive theorem proving. I'm looking forward to seeing what Lean 4 brings to the table when it's released.