Behind Wolfram Alpha’s Mathematical Induction-Based Proof Generator | Hacker News Reader

Behind Wolfram Alpha’s Mathematical Induction-Based Proof Generator

blog.wolfram.com

73 pointseusebio6 comments

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...

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.

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.

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

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.

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.

Reply on news.ycombinator.com