Behind Wolfram Alpha’s Mathematical Induction-Based Proof Generator

aab0 · on July 15, 2016

It seems kind of strange that he never thought of using computer proof systems for checking whether his proofs were right in class, and that he took a pattern-matching approach rather than using any of the existing AI proof-deriving systems like https://arxiv.org/abs/1606.04442 or https://intelligence.org/2013/12/21/josef-urban-on-machine-l...

fmap · on July 16, 2016

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.

squobias · on July 16, 2016

There is literally almost a century of research in this area, and even a decade+ of much more impressive work on the natural language front.

If you care about anything beyond problem sets in freshman math courses, this post is noise, not signal.

auggierose · on July 16, 2016

Well, that century of research can be summed up like this: There is no good induction based proof generator.

squobias2 · on July 16, 2016

That's simply not true. This isn't the first, and it's very, very likely not the best.

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.

auggierose · on July 16, 2016

It seems to me that all of these approaches are very limited in scope (mainly linear arithmetic), and only capable of analysing pretty simple programs. That's not the kind of induction proofs I deal with on a daily basis, which prove arbitrary mathematical theorems. For those things you need to use just hard manual sweat work.