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.