3 ms·
I don't think that computers have an advantage because they can navigate search spaces efficiently. The search space for difficult theorems is gigantic. Proving
by tim-kt 2y ago
I don't think that computers have an advantage because they can navigate search spaces efficiently. The search space for difficult theorems is gigantic. Proving them often relies on a combination of experience with rigorous mathematics and very good intuition [1] as well as many, many steps. One example is the classification of all finite simple groups [2], which took about 200 years and a lot of small steps. I guess maybe brute forcing for 200 years with the technology available today might work. But I'm sceptical and sort of hope that I won't be out of a job in 10 years. I'm certainly curious about the current development.
[1] https://terrytao.wordpress.com/career-advice/theres-more-to-mathematics-than-rigour-and-proofs/ https://terrytao.wordpress.com/career-advice/theres-more-to-...
[2] https://en.m.wikipedia.org/wiki/Classification_of_finite_simple_groups https://en.m.wikipedia.org/wiki/Classification_of_finite_sim...
- thrance 2y agoOh for sure, when I say "soon" it's only relative to AGI. What I meant to convey, is that theorem proving at least is a well-defined problem, and computers have had some successes in similar-ish search problems before. Also I don't think pure brute-force was ever used to solve any kind of interesting problem. Chess engines make use of alpha-beta pruning plus some empirical heuristics people came up with over the years. Go engines use Monte-Carlo Tree Search with straight deep learning models node evaluation. Theorem proving, when it is solved, will certainly use some kind of neural network.