3 ms·
> a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible Have you got some links? Sounds very intere
by lordnacho 6y ago
> a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible
Have you got some links? Sounds very interesting.
- a_humean 6y agoHe is refering to the late 19th and early 20th century work on the foundations of mathematics amoung mathematicans and philosophers. They attempted to fully formalise mathematics. Serveral approaches and schools in mathematics all hit various paradoxes, often of the same kind, and this ultimately culminated in Godel's incompleteness theorems: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... https://plato.stanford.edu/entries/goedel-incompleteness https://plato.stanford.edu/entries/goedel-incompleteness
- umvi 6y agoThere's also a thing called "the halting problem" which is related to this. Because without the halting problem you could solve any mathematical proof by simply turning it into a computer program that brute forces the problem domain and calculating whether the the program will terminate or not. Of course, this is impossible.
- sukilot 6y agoThat's a bit backwards. The halting problem is a computer-flavored variant of Gödel's work. A very simple part -- it's essentially a computer program that says "The program that produced this string is lying".