7
$\begingroup$

It's probably possible to prove that P ≠ NP, that one-way functions exist, and that parity games cannot be solved in polynomial time (yes, I've been reading through this list), but how would we go about proving any of those things? Have there been any proofs to any computer science theories, or answers to any substantial computer science questions (such as the ones in that list)? Are they like mathematical proofs (such as Grigori Perelman's resolution to the Poincaré conjecture)? I know that the P versus NP problem seems out of my league, being a junior in high school, but it's a problem that intrigues me, and I would really like to see how others (if any) have answered other, related questions, because I would like to look into a resolution to the problem.

This isn't a duplicate of this question primarily because physics isn't computer science, and secondarily because, unless I'm mistaken, computer science theories are not proven the same way that theories related to physical sciences are proven. They're more like mathematical proofs in that they're logical (right?).

$\endgroup$
  • $\begingroup$ Parity games can now at least be solved in quasipolynomial time, see this answer. Maybe it is not so important after all, that they cannot be solved in polynomial time. They can be solved in practice, and that is what counts most. $\endgroup$ – Thomas Klimpel Mar 12 '17 at 20:05
8
$\begingroup$

I would disagree on a few counts.

I don't think it's "probably" possible to prove $P \neq NP$. I certainly don't think it's impossible, but Gödel's incompleteness theorems tell us that there are some sentences in a logical system which are true but which can't be proven.

You ask if there have been proofs to Computer Science theories. There have been thousands at the very least. These vary from insignificant to huge. I'll mention some of the most relevant (aka my favorite) ones here.

  • Some problems cannot be solved by ANY algorithm. No matter what. Ever. An example of this is determining if a computer program will run forever. There is no way to look at a program and be guaranteed a yes/no answer for if it will run forever.
  • The functions which can be computed by a Turing Machine are the same as functions which can be computed by the lambda calculus, are the same as practically every programming language. Basically, though speed might differ, all turing-complete programming languages (which is most of them) can solve the same set of problems.
  • The types of a computer program are directly related to its proof of correctness. This is called the "Curry-Howard Correspondence", and is quite complex, so I won't go into the details here. Note that by types I mean things like integer, string, list, array, etc.
  • A list of real numbers can't be sorted in faster than $\Omega (n\log n).$ This means that no matter what algorithm you use, in the worst case it will take approximately $n\log n$ steps to sort that list.
  • A large number of problems are, at their core, the same problem. If you've ever heard of NP-complete problems, what that means is that these problems all boil down to satisfiability. They are from graph theory, combinatorics, scheduling, and a variety of areas, but ultimately, they are all just checking if there's some input to a logical formula of ORs and ANDs which will spit out true as the overall result.

Note that these are all necessarily complex topics, which I have simplified to give you a taste of the sort of things provable in computer science.

You ask how Computer Science theories are proven. The problem is that Computer Science is an incredibly diverse field, and it really depends on your sub-field. Theory of computation, programming language construction and formal AI ("neat" AI) are highly mathematical, and are based heavily on logic and proofs.

However, there are many sub-fields which are much more experimental. Human-Computer interaction or anything having to do with the human side of computing will rely heavily on studies and experiments involving users. Operating Systems, Graphics and Compilers will rely heavy on performance evaluations, seeing which programs are fastest in the real word, not just on paper.

If you are in Junior High, I think there are many computer science problems which are in your reach. Because it is such a young field, there are many unsolved CS problems which are relatively simple to understand. Unlike physics, where you need tons and tons of calculus background, CS really relies on simple logic. If you can learn induction, logic and the basics of discrete structures (graphs, strings, etc.), I think there are probably lots of concepts that are accessible to a Junior High student.

$\endgroup$
10
$\begingroup$

Theoretical computer science, to which the questions you state belong, is part of mathematics, and the methods used to resolve questions are the same ones used elsewhere in math, namely the method of proofs. The questions you list are notoriously difficult, and seem to be out of reach for current methods.

In the past, the methods used to attack questions of the sort you describe were purely combinatorial. Recently, Ketan Mulmuley and his students have come up with a different method which employs representation theory (via some algebraic geometry), and is conjectured by them to be one day strong enough to resolve the P versus NP question. Currently, though, the only questions within reach of their methods are algebraic ones like permanent versus determinant rather than Boolean ones like P versus NP.

Since it is widely (though not universally) believed that P is different from NP, many results are proved conditional on this assumption. That is, they hold only if P is indeed different from NP. The area of hardness of approximation, which studies how well different combinatorial problems can be approximated in the worst case (in polynomial time), is a good example: all results in this area are conditional on P versus NP or on some even stronger assumptions.

$\endgroup$
4
$\begingroup$

when you say its "probably possible" to solve key/hardest unsolved open problems in CS that is mere "beginners mind" or [more harshly but honestly, uninformed-] speculation. anyone who realizes that eg P vs NP has been open for over 4 decades [over double your own age!] will have to admit that its long history of no resolution, and an unclaimed $1M prize over a decade old, are some circumstantial evidence the possibility of unprovability is not negligible. as I read a poll of theorists,[2] about 4-5% say they think its unprovable or equivalently, "independent" of basic arithmetic axioms (it is indeed apparently a small minority view among experts).

there is even an award-winning paper by Razborov/Rudich called Natural Proofs that, under some interpretations, gives some evidence of unprovability, by showing [roughly, informally] such a proof if it exists must be fundamentally different from any known "similar" proofs ever devised (or in a strictly defined formal sense "unnatural"!). & you should learn about problems that were proven undecidable after long being open eg Hilberts 10th problem (open ¾-century).

yes, most major CS proofs at the core are math proofs "under the hood", sometimes highly technical, using elements of eg combinatorics, extremal graphs & extremal combinatorics. the nearest existing proofs to P$\neq$NP are arguably proofs by Razborov & later researchers about monotone circuit lower bounds. there is an undergraduate level presentation [possibly the most accessible ever published] in Models of Computation by Savage. see also Lance Fortnows new book, The Golden Ticket.

as an exotic/longshot wildcard footnote, there is some speculation and enthusiasm in math & TCS even by some elite experts (eg WT Gowers) that automated proof technology might someday become much more powerful eg semi-creative and almost AI-like.[1] sci-fi scenarios aside, nevertheless it has succeeded with breakthroughs at times on some isolated but very difficult problems such as the 4 color theorem and Keplers conjecture.

another approach for P vs NP might be to work from a proposed proof outline[3] or team up with other people working on the problem.[4][5][6]

[1] adventures & commotions in automated theorem proving, vzn

[2] P vs NP poll by Gasarch

[3] outline for a NP vs P/poly proof based on monotone circuits, hypergraphs, factoring, and slice functions, vzn

[4] Jun Fukuyama P vs NP page

[5] monotone circuits tcs.se chat room

[6] RJ Lipton P vs NP blog

$\endgroup$
  • 2
    $\begingroup$ Fermat's last theorem was open for a long time. It just had to wait for the proper techniques. There is no reason to believe that P vs. NP is unsolvable just because no one could solve it in the first few decades. $\endgroup$ – Yuval Filmus May 10 '13 at 2:53
  • 1
    $\begingroup$ no argument. but remember there are far, far mathematicians alive today than have ever been alive in history, probably, and the sophistication of that existing math is extraordinary. btw, personally think P vs NP is provable. $\endgroup$ – vzn May 10 '13 at 3:31
  • 1
    $\begingroup$ Mathematicians today are large in number but they also pursue vastly more areas. Most mathematicians today, needless to say, aren't trying to solve P vs. NP. $\endgroup$ – Yuval Filmus May 10 '13 at 3:46
  • 2
    $\begingroup$ most major CS proofs at the core are math proofs "under the hood" — It would be more accurate to say all CS proofs are "math proofs", because that's what the word "proof" means. $\endgroup$ – JeffE May 10 '13 at 14:47
  • $\begingroup$ CS has its own language. math has its own language. there is strong overlap, but its not the same. math is much older than CS. there are aspects/elements/structures of CS proofs not part of older math. for example, circuits. but yes, those reduce to graphs (which are old). also, large swathes of modern math dont (yet? seem to?) have application in CS. etc. re "not many mathematicians attempting to solve P vs NP". think the problem has gotten very large/intense effort by top minds inside/outside CS, think top CS researchers would agree. there is much related research. $\endgroup$ – vzn May 10 '13 at 15:06
0
$\begingroup$

The resolved ones obviously aren't on that list... burning questions were the halting problem, what is meant by "algorithm", defining a reasonably "machine independent" way of saying when a solution to a problem is "efficient". The analysis of algorithms is a completely new area, with a rich collection of results. The list goes on.

$\endgroup$
  • 3
    $\begingroup$ The analysis of algorithms is a completely new area — ...dating back to either the 1960s or ancient Egypt, depending on how generously you set the boundaries. $\endgroup$ – JeffE May 10 '13 at 14:48

Not the answer you're looking for? Browse other questions tagged or ask your own question.