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.
If you care about anything beyond problem sets in freshman math courses, this post is noise, not signal.
Google the term invariant generator. There are many impressive inductive invariant generators for interesting and challenging theories that contain the sorts of formulas this tool appears to handle (ie that summation is for loop).
In fact, the field of inductive invariant generation is so well-established that there are de facto benchmarks that the author could evaluate his work against, if he cared to make the claim you've made here.
Going from an inductive invariant to an informal English prose proof is slightly less well-trodden territory, but this isn't the first piece of work to do that, either.
I don't mean to disparage the product innovation here, but that first sentence needs to be edited out. Perhaps the right way of saying this is that the step-by-step integral solver for WolframAlpha is a really nice product, but it would have been dishonest to claim it was the first algorithm for computing indefinite integrals.