Most Popular
1500 questions
29
votes
1 answer
Is there a reasonable automated proof system for TCS theorems?
Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I downloaded and experimented with Coq, but it…
user1338
29
votes
0 answers
Does $EXP\neq ZPP$ imply sub-exponential simulation of BPP or NP?
By simulation I mean in the Impaglazzio-Widgerson [IW98] sense, i.e. sub-exponential deterministic simulation which appears correct i.o to every efficient adversary.
I think this is a proof: if $EXP\neq BPP$ then from [IW98] we get that BPP has such…
Sebastian Ben Daniel
- 827
- 5
- 9
29
votes
1 answer
What's the status of Babai's Graph isomorphism result?
It's been over a year since his January 2017 retraction and correction.
Is there news?
If not is this normal for validation to take this long? I would expect it would get plenty of attention.
Has anyone of note spoken up to support/doubt the…
Meir Maor
- 434
- 5
- 11
29
votes
6 answers
Why naturals instead of integers?
I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, Types and Programming Languages). Description of the…
Artem Pelenitsyn
- 1,103
- 6
- 20
29
votes
1 answer
Has a proof checker bug ever invalidated a major proof?
Most (all?) proof assistants have soundness bugs fixed on occasion. However, from those I've seen these bugs are usually difficult to come across unintentionally, and results proved before the bug is fixed generally hold up after the fix.
Three…
Geoffrey Irving
- 3,253
- 15
- 29
29
votes
2 answers
Conditions for NFA universality
Consider a nondeterministic finite automata $A = (Q, \Sigma, \delta, q_0, F)$, and a function $f(n)$. Additionally we define $\Sigma^{\leq k} = \bigcup_{i \leq k} \Sigma^i$.
Now lets analyze the following statement:
If $\Sigma^{\leq f(|Q|)}…
Mike B.
- 749
- 6
- 13
29
votes
7 answers
Proving lower bounds by proving upper bounds
The recent breakthrough circuit complexity lower-bound result of Ryan Williams provides a proof technique that uses upper-bound result to prove complexity lower-bounds. Suresh Venkat in his answer to this question, Are there any counter-intuitive…
Mohammad Al-Turkistany
- 20,928
- 5
- 63
- 149
29
votes
1 answer
Finding a biased coin using a few coin tosses
The following problem came up during research, and it's surprisingly clean:
You have a source of coins. Each coin has a bias, namely a probability that it falls on "head".
For each coin independently there's probability 2/3 that it has bias at…
Dana Moshkovitz
- 10,979
- 1
- 50
- 77
29
votes
4 answers
If P = NP were true, would quantum computers be useful?
Suppose that P = NP is true. Would there then be any practical application to building a quantum computer such as solving certain problems faster, or would any such improvement be irrelevant based on the fact that P = NP is true? How would you…
user1338
29
votes
3 answers
Problems in $\mathsf{BPP}$ not known to be in $\mathsf P$?
What problems are known to belong to $\mathsf{BPP}$ but not known to belong to $\mathsf P$?
More precisely, I am interested in independent problems, that is whose derandomizations are not known to be equivalent. For instance, it is known that…
Bruno
- 4,449
- 33
- 45
29
votes
2 answers
Tight Lower bounds on Savitch's theorem
First of all, I apologize in advance for any stupidity. I am by no means an expert on complexity theory (far from it! I am an undergraduate taking my first class in complexity theory) Here's my question. Now Savitch's Theorem states that…
gabgoh
- 1,548
- 12
- 22
29
votes
7 answers
Nontrivial membership in NP
Is there an example of a language which is in $NP$, but where we cannot prove this fact directly by showing that there exists a polynomial witness for membership in this language?
Instead, the fact that the language is in $NP$ would be proven by…
Denis
- 8,843
- 28
- 55
29
votes
4 answers
Bounded-cardinality bounded-frequency set cover: hardness of approximation
Consider the minimum set cover problem with the following restrictions: each set contains at most $k$ elements and each element of the universe occurs in at most $f$ sets.
Example: the case $k = 4$ and $f = 2$ is equivalent to the minimum vertex…
Jukka Suomela
- 11,500
- 2
- 53
- 116
29
votes
2 answers
Can you identify the sum of two permutations in polynomial time?
There were two questions asked recently on cs.se which were either related to or had a special case equivalent to the following question:
Suppose you have a sequence $a_1, a_2, \ldots a_n$ of $n$ numbers such that $\sum_{i=1}^n a_i = n(n+1).$ …
Peter Shor
- 24,763
- 4
- 93
- 133
29
votes
2 answers
What are the consequences of Parity-L = P?
Parity-L is the set of languages recognized by a non-deterministic Turing machine which can only distinguish between an even number or odd number of "acceptance" paths (rather than a zero or non-zero number of acceptance paths), and which is further…
Niel de Beaudrap
- 8,821
- 31
- 70