On effective proofs for solvable problems 

Associate Professor Jakob Nordström will receive funding from the Knut and Alice Wallenberg Foundation to recruit an international researcher for a postdoctoral position at the School of Computer Science and Communication, KTH Royal Institute of Technology, Stockholm. 

If there is a rapid, computer-aided verification of a solution to a mathematical problem, is it also possible to find an algorithm to quickly solve it too? This question is closely related to the most important conjecture in theoretical computer science, the P versus NP problem. For example, a computer can quickly verify the existence of a solution to the question of whether a set of integers, say 3, 8, 13, 14, 16, contain a subset which add up to 25. The answer is yes, because 3 + 8 +14 = 25. Even for a very large set, it is still very easy to rapidly verify a given solution. But there is no known algorithm that can provide the solution within a reasonable time. 

P equals NP means that it is possible to create such a fast algorithm. However, many mathematicians believe that the conjecture is false, i.e. that there are problems of this kind that cannot be solved by a fast computer, although nobody has been able to prove it. The first person to prove or disprove the conjecture will receive USD 1 million from the Clay Mathematics Institute which, in 2000, established the prize for solving any of the seven most important problems for the coming millennium. 

The P vs. NP problem has founded a new field of research called proof complexity. There are many reasons to study proof complexity. One is that research on formal proof systems may lead to a solution of the P vs. NP problem. Another is that such research may also develop a way of measuring how deep mathematically valid statements are. In other words, one may be able to establish how powerful a proof system is necessary to show that families of already known mathematical statements are true. 

In addition, proof complexity is one of the few tools available for studying SAT solvers. These are computer programs that are successfully used in many applications, including hardware and software verification, artificial intelligence, cryptography, computational biology, and even pure mathematics. The project’s aim is to research the strengths and deficiencies of a variety of proof systems. 

Photo: KTH Royal Institute of Technology