Stephen Cook, at the University of Toronto, published in 1971 "The Complexity of Theorem-Proving Procedures", formulating with mathematical precision the question that would become the most important open problem in theoretical computer science: whether every problem whose solution can be verified quickly (in polynomial time, class NP) can also be solved quickly from scratch (class P), or whether there exist problems fundamentally harder to solve than to check. Cook shows that the Boolean satisfiability problem (SAT) — determining whether there is a true/false assignment making a given logical formula true — is "NP-complete": any other problem in NP can be translated into an instance of SAT in polynomial time, so that if someone found a fast algorithm to solve SAT, they would automatically have a fast algorithm for solving every problem in NP. The result, discovered independently by Leonid Levin in the Soviet Union the same year (hence its alternative name, the Cook-Levin theorem), lays the foundations of NP-completeness theory, which Richard Karp would extend in 1972 to 21 other classic problems. The P versus NP question remains unsolved and is one of the seven "Millennium Prize Problems" of the Clay Mathematics Institute, carrying a one-million-dollar prize for whoever proves or disproves it.