Elon Musk threw nine-figure promises at top AI researchers

semafor.com

22 pointsmfiguiere2 comments

funny how AI started as logic and theorem proving in the 70s, but that was too hard, so now statistical approaches based on vast swaths of data being memorized are used to solve different problems. but now Musk and his team think those approaches can go back and solve the original problems.

i don’t see how statistical approaches can help an AI construct a mathematical proof of even some “simple” problem like the Collatz conjecture. you can’t just hallucinate an implication between two theorems because there’s a high probability. proofs have to have clear, detailed reasoning that can be verified and understood by humans.

cutting edge theorem proving systems like Coq with automated checking have serious limitations like bounded recursion, so you can’t just let a trial-and-error search run for a while because it may not be provable in the system at all.

Statistical approaches are good for telling us where to look, and then we still have the symbolic approaches to precisely construct the correct proofs. I do research on the symbolic part and the statistical approach has a lot to offer, like suggesting what bits are likely to be used in a given proof context. Then there is a whole lot of stuff with Neuro-symbolic “AI” where the search efficiency of ANNs are leveraged. But yeah, you can’t “smoke and mirrors” your way to generating a proof like you can with generating natural languages (GPTs) but it is not that far out I think.

Reply on news.ycombinator.com