In particular, there has been a ton of work on automating inductive proofs. So while I enjoyed the article, I'm not sure what's up with the first sentence. Thi

In particular, there has been a ton of work on automating inductive proofs. So while I enjoyed the article, I'm not sure what's up with the first sentence. This is definitely not the first inductive theorem prover. Funnily enough, the most advanced prover with auto induction (ACL2) is also based on pattern matching and cleverly chosen heuristics. There are more specialized methods such as rippling, implicit induction, etc., but making this work well is apparently difficult.