Questions tagged [proofs]

Used for questions about existing or possible proofs of a specific theorem or conjecture

Filter by
Sorted by
Tagged with
96 votes
9 answers
20k views

What would it mean to disprove Church-Turing thesis?

Sorry for the catchy title. I want to understand, what should one have to do to disprove the Church-Turing thesis? Somewhere I read it's mathematically impossible to do it! Why? Turing, Rosser etc ...
user avatar
57 votes
18 answers
2k views

Where and how did computers help prove a theorem?

The purposes of this question is to collect examples from theoretical computer science where the systematic use of computers was helpful in building a conjecture that lead to a theorem, falsifying a ...
51 votes
8 answers
5k views

Are there non-constructive algorithm existence proofs?

I remember I might have encountered references to problems that have been proven to be solvable with a particular complexity, but with no known algorithm to actually reach this complexity. I struggle ...
jkff's user avatar
  • 8,951
46 votes
4 answers
4k views

Are there any proofs the undecidability of the halting problem that does not depend on self-referencing or diagonalization ?

This is a question related to this one. Putting it again in a much simpler form after a lot of discussion there, that it felt like a totally different question. The classical proof of the ...
Mohammad Alaggan's user avatar
44 votes
8 answers
3k views

Rigour leading to insight

On MathOverflow, Timothy Gowers asked a question titled "Demonstrating that rigour is important". Most of the discussion there was about cases showing the importance of proof, which people on ...
András Salamon's user avatar
35 votes
4 answers
1k views

Proofs that expose a deeper structure

The standard proof of the Chernoff bound (from the Randomized Algorithms textbook) uses the Markov inequality and moment generating functions, with a bit of a Taylor expansion thrown in. Nothing too ...
30 votes
4 answers
5k views

Implications of unprovability of $P\neq NP$

I was reading "Is P Versus NP Formally Independent?" but I got puzzled. It is widely believed in complexity theory that $\mathsf{P} \neq \mathsf{NP}$. My question is about what if this is ...
karthik's user avatar
  • 417
29 votes
4 answers
938 views

Proofs obtained only through spectral graph theory

I have an increasing interest in spectral graph theory, which I find fascinating, and I've started collecting a few documents that I have yet to read more thoroughly than what I so far have. However, ...
Anthony Labarre's user avatar
29 votes
1 answer
5k views

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 ...
Meir Maor's user avatar
  • 434
27 votes
5 answers
948 views

Quantum proofs of classical theorems

I'm interested in examples of problems where a theorem which seemingly has nothing to do with quantum mechanics/information (e.g. states something about purely classical objects) can nevertheless be ...
Marcin Kotowski's user avatar
25 votes
4 answers
3k views

Proofs, Barriers and P vs NP

It is well known that any proof resolving the P vs NP question must overcome relativization, natural proofs and algebrization barriers. The following diagram partitions the "proof space" into ...
Shiva Kintali's user avatar
23 votes
4 answers
6k views

Proof of the pumping lemma for context-free languages using pushdown automata

The pumping lemma for regular languages can be proved by considering a finite state automaton which recognizes the language studied, picking a string with a length greater than its number of states, ...
a3nm's user avatar
  • 9,269
20 votes
3 answers
1k views

Examples of the value of proofs for algorithms

In teaching Intro. Algorithms to undergrads, one of the most difficult tasks is to motivate why they need to know how to prove things about algorithms. (For many students, at least in many US ...
Joshua Grochow's user avatar
16 votes
2 answers
1k views

Complexity of counting the number of edge covers of a graph

An edge cover is a subset of edges of a graph such that every vertex of the graph is adjacent to at least one edge of the cover. The following two papers say that counting edge covers is #P-complete: ...
a3nm's user avatar
  • 9,269
15 votes
1 answer
1k views

Examples of algorithms and proofs that seem correct, but aren't

In my intro to programming course, we're learning about the Initialization-Maintenance-Termination method of proving an algorithm does what we expect it to. But we've only had to prove that an ...
Marin's user avatar
  • 153
15 votes
1 answer
468 views

Natural theorems proven only "to high probability"?

There are plenty of situations where a randomized "proof" is much easier than a deterministic proof, the canonical example being polynomial identity testing. Question: Are there any natural ...
Geoffrey Irving's user avatar
14 votes
1 answer
651 views

How is the MA version of SETH proven to be false?

According to this paper, which discusses a nondeterministic extension of the Strong Exponential Time Hypothesis (SETH), "[…] Williams has recently shown related hypotheses about Merlin-Arthur ...
user avatar
13 votes
4 answers
4k views

Proof of Levenshtein distance

In the article Levenshtein distance Wikipedia says about the proof of invariant that: This proof fails to validate that the number placed in d[i,j] is in fact minimal; this is more difficult to ...
Nutel's user avatar
  • 381
13 votes
2 answers
1k views

An Interactive Proof of God's Number?

I've been learning about interactive proofs lately and I've been wondering if the whole thing was nothing more than a theoretical curiosity, or if it had any practical applications. I thought I'd ...
gabgoh's user avatar
  • 1,548
13 votes
2 answers
5k views

Simple proof of Ω(n lg n) worst-case bound for uniqueness/distinctness?

There are several proofs for the loglinear lower bound for the element uniqueness/distinctness problem (based on algebraic computation trees or adversarial arguments), but I'm looking for one that's ...
Magnus Lie Hetland's user avatar
13 votes
1 answer
1k views

Correctness proofs of classic Paxos and Fast Paxos

I am reading the "Fast Paxos" paper by Leslie Lamport and get stuck with the correctness proofs of both classic Paxos and Fast Paxos. For consistency, the value $v$ picked by the coordinator in phase ...
hengxin's user avatar
  • 2,329
12 votes
1 answer
2k views

Why is Feige-Fiat-Shamir not Zero Knowledge without sign bits?

In chapter 10 of HAC (10.4.2), we see the well-known Feige-Fiat-Shamir identification protocol based on a zero-knowledge proof using the (presumed) difficulty of extracting square roots modulo a ...
Fixee's user avatar
  • 1,003
11 votes
3 answers
811 views

Where do I turn for help with research/publishing?

I have been developing a SAT algorithm for a while, and have reached a point where I'd like to share it. I don't know many people in computer science, and I'm not sure exactly where to turn. I'm ...
Matt Groff's user avatar
  • 2,100
11 votes
3 answers
633 views

Proofs found by computer

In 1996, a long-standing open problem was solved by a computer; namely, that Robbins algebra and Boolean algebra are the same. The proof was found by an automated theorem prover. Moreover, the known ...
Mahdi Cheraghchi's user avatar
11 votes
2 answers
2k views

On the provability of P versus NP

First of all, my understanding on Gödel's incompleteness theorem (and formal logic in general) is very naive, also is my knowledge on theoretical computer science (meaning only one graduate course ...
Alvaro's user avatar
  • 145
10 votes
0 answers
262 views

How would proof of the Lindelöf hypothesis improve our understanding of computational complexity classes?

A recent press release from the Viterbi School of Engineering at USC discussed the proof of the Lindelöf hypothesis by Athanassios Fokas, a visiting professor from the Department of Applied ...
Greenstick's user avatar
8 votes
3 answers
594 views

Would a proof assuming a physical law be considered sufficient?

I've always wondered if proofs in computer science would be considered sufficient proofs of the proposition if they needed to assume physical laws? For example, I'm wondering what would happen if ...
user541686's user avatar
8 votes
1 answer
606 views

Humanifying computer-generated or computer assisted proofs

I remember reading a blog post displaying two versions of the same proof, one written by a human and the other by a machine, and asked the readers to tell which is which. Trying to google the post ...
SorcererofDM's user avatar
8 votes
1 answer
139 views

Construction of arbitrary functions with exponential-size $MODp \circ MODq$ circuits

It is mentioned in multiple papers [1], [2] that $MODp \circ MODq$ circuits for two distinct primes $p, q$ can compute arbitrary functions in exponential size. However, [1] provides no citation for ...
Jake's user avatar
  • 1,214
8 votes
1 answer
141 views

How to prove relations between "classes" of types?

After reading Effects as Sessions, Sessions as Effects, I was wondering how would a proof of equivalence between both take place, or even, a proof of Sessions types being a Type and Effect System. In ...
cyberglot's user avatar
  • 181
7 votes
2 answers
790 views

Proof Strategies on P versus BPP

Typically to show $P=NP$, one has to show an NP complete problem has a polynomial time solution and to show $P\neq NP$, has to show an NP complete problem has superpolynomial lower bound. These are ...
Turbo's user avatar
  • 12.9k
7 votes
1 answer
205 views

Document references describing weaknesses for cutting planes and algebraic proof system?

Here, Fortnow says (section 4.3): Since then complexity theorists have shown similar weaknesses in a number of other proof systems including cutting planes, algebraic proof systems based on ...
Jérôme Verstrynge's user avatar
7 votes
1 answer
158 views

Conversion between NP certificates

This might be a well-known fact, but I can't convince myself of whether this is true. Suppose I have some NP language and two different verifying procedures V and V' for L. For any x in L, is it the ...
Noel Arteche's user avatar
7 votes
1 answer
412 views

Where is the quote "Informal proofs are algorithms, formal proofs are code" from?

Does anyone know the origin of the quote, Informal proofs are algorithms; formal proofs are code. Its made in Benjamin C. Pierce et al.'s Software Foundations.
Steven Shaw's user avatar
7 votes
1 answer
338 views

Proof Haar matrices satisfy JL lemma

The Johnson-Lindenstrauss lemma says roughly that for any collection $S$ of $n$ points in $\mathbb{R}^d$, there exists a linear map $f:\mathbb{R}^d \rightarrow \mathbb{R}^k$ where $k = O(\log n/\...
hoom's user avatar
  • 101
6 votes
1 answer
405 views

Would an optimal sorting network ever have to swap two numbers the "wrong" way

Intuitively it seems like an optimal (either minimum depth or minimum gates) sorting network should never have to compare-swap two numbers the "wrong" way (such that the larger one goes into the ...
dspyz's user avatar
  • 916
6 votes
2 answers
5k views

What techniques are used for proving algorithms optimal? [duplicate]

Possible Duplicate: Problems that can be used to show polynomial time hardness results Given a polynomial time algorithm, what techniques are known for proving that an algorithm is optimal? E.g.,...
user avatar
6 votes
0 answers
208 views

More elementary proof of coloring theorem for d x d^2 rectangles

The following is known: For all $c$, for all $c$-colorings of $N\times N$ there exists a $d \times d^2$ rectangle ($d \ge 2$) such that all four corners are the same color. The proof uses the Poly-...
Bill GASARCH's user avatar
5 votes
1 answer
170 views

Establishing competing memory limits for pushdown automata

Let $L$ be the language of all even-length strings whose first half is a palindrome. Let $L$ be the language of all even length strings whose first half is imbalanced—with an unequal number of $\...
user326210's user avatar
5 votes
0 answers
263 views

What's wrong with this $P \neq BPP$ proof?

I developed this simple argument while learning about the $BP$ operator and McCreight and Meyer's Union Theorem, however I cannot pinpoint where my error is. By the Union Theorem, there exists a total ...
trillianhaze's user avatar
5 votes
0 answers
317 views

Geometric / Visual explanation that the average height of a random binary tree of given size $n$ is asymptotically $2\sqrt{\pi n}$

I just finished reading the proof that the average height of a random binary of given size $n$ is asymptotically $2\sqrt{\pi n}$. I'm now searching for an intuitive, or geometric, or visual proof of ...
Clément's user avatar
  • 281
4 votes
1 answer
501 views

Proof that the graph optimization problem is NP-hard

I'm trying to prove that the following optimization problem is NP-hard: Given a graph $G=(V,E)$, non-negative vertex weight functions $w(v)$ and $s(v)$, and a non-negative edge weight function $t(u,v)...
marszall87's user avatar
4 votes
3 answers
424 views

Proving proof system properties within the proof system itself?

While reading about Frege proof systems in [1], I came across the completeness theorem and its proof, which involves a few lemmas introduced first. Here are the first two of those lemmas: $$\begin{...
user avatar
4 votes
2 answers
120 views

Proving that a given formula in LTL is the smallest way to express it

I am looking for a way to prove that a given LTL formula is expressed with the fewest number of temporal operators possible. I would like to do this to compare the expressive length with other ...
Gokul's user avatar
  • 43
4 votes
1 answer
239 views

Halting problem proofs that do not utilise self-reference or diagonalization

Are there any proofs of the Halting problem that do not involve any self-reference, and diagonalization (or any diagonal argument) whatsoever? All the duplicate questions I have come across end up ...
Alan Whitteaker's user avatar
4 votes
1 answer
196 views

Explanation of 1-generic to prove undecidability of halting problem

This question is about an answer in question Are there any proofs the undecidability of the halting problem that does not depend on self-referencing or diagonalization ? Bjørn Kjos-Hanssen answer ...
user14000's user avatar
4 votes
0 answers
181 views

Any problems for which we know the complexity, but no algorithms with the same time?

I suddenly found myself wondering if there are any problems for which the complexity (time or space or anything else) is proven, say to be O(n^2), but for which the best known algorithms are worse ...
MinusPi's user avatar
  • 59
3 votes
1 answer
702 views

Possible to do Complexity theory with only counting and Pigeonhole

Most of the proofs in the book Computational complexity by Barak and Arora seem to be Pigeonhole in disguise. What are some places in Complexity theory where counting and Pigeonhole was insufficient ...
Turbo's user avatar
  • 12.9k
3 votes
3 answers
1k views

What's wrong with this proof that NP=Co-NP implies NP=PSPACE

Below is a short informal proof that NP=co-NP implies NP=PSPACE. What's wrong with the proof? Assuming NP=co-NP, an instance F of TQBF can be solved by a polynomial NDTM this way: Non-...
Ajay's user avatar
  • 147
3 votes
2 answers
717 views

Formally proving no algorithm exists [closed]

Are there standard techniques to show that no algorithms exist for given complexity constraints? For example, consider the following problem. The input is a list of items with exactly one duplicate, ...
user890123818239's user avatar