Hacker News new | ask | show | jobs
by lioeters 1368 days ago
Opening paragraphs of the linked paper:

> In 1900, David Hilbert challenged mathematicians to design a “purely mechanical procedure” to determine the truth or falsehood of any mathematical statement. That goal turned out to be impossible. But the question — does such a procedure exist, and why or why not? — helped launch two related revolutions that shaped the twentieth century: one in science and philosophy, as the results of G ̈odel, Church, Turing, and Post made the limits of reasoning itself a subject of mathematical analysis; and the other in technology, as the electronic computer achieved, not all of Hilbert’s dream, but enough of it to change the daily experience of most people on earth.

> Although there’s no “purely mechanical procedure” to determine if a mathematical statement S is true or false, there is a mechanical procedure to determine if S has a proof of some bounded length n: simply enumerate over all proofs of length at most n, and check if any of them prove S. This method, however, takes exponential time. The P ?= NP problem asks whether there’s a fast algorithm to find such a proof (or to report that no proof of length at most n exists), for a suitable meaning of the word “fast.” One can think of P ?= NP as a modern refinement of Hilbert’s 1900 question. The problem was explicitly posed in the early 1970s in the works of Cook and Levin, though versions were stated earlier—including by G ̈odel in 1956, and as we see above, by John Nash in 1955.

> Think of a large jigsaw puzzle with (say) 101000 possible ways of arranging the pieces, or an encrypted message with a similarly huge number of possible decrypts, or an airline with astronomically many ways of scheduling its flights, or a neural network with millions of weights that can be set independently. All of these examples share two key features:

> (1) a finite but exponentially-large space of possible solutions; and

> (2) a fast, mechanical way to check whether any claimed solution is “valid.”