# Tagged Questions

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

1answer
185 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.
2answers
100 views

### Are equalizers of regular functions always regular languages? (My guess is no because PCP, but…)

Edit: I originally defined a regular function as a function computable by a Mealy machine, but Denis pointed out that that was a weaker model than what I was thinking of. So to be more precise, by a "...
0answers
158 views

### New proofs from “The Book” [closed]

The book "Proofs from The Book", referencing Erdős' notion of God's book, which contains the most beautiful proofs, was published in 1998. Are there any new proofs that should be considered for "...
1answer
96 views

### Paxos made simple, invariant P2c

I am reading Leslie Lamport's Paxos Made Simple paper. Can someone explain why $P2^c$ implies $P2^b$? $P2^b$ If a proposal with value $v$ is chosen, then every higher-numbered proposal ...
1answer
496 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 ...
0answers
58 views

### Looking for reference proving polynomial-time bounds for A* search under specific conditions

In the textbook "Artificial Intelligence - A Modern Approach" (Russel, Norvig), it mentions that a sufficient criteria for the A* search algorithm to complete in polynomial time is for the heuristic ...
3answers
244 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 ...
1answer
545 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 ...
1answer
100 views

### Undecidable Single Programs [closed]

So the halting problem basically states that there cannot exist any finite length algorithm for automatically verifying if other finite length algorithms terminate. But suppose I start listing out ...
0answers
70 views

### Minimum size counter-example in a 2-machine scheduling problem proof

I'm confused about something in the main proof in this paper (sorry that it's behind a paywall, but I assume many people on here have access to such things through their university and my posting the ...
1answer
449 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 ...
0answers
63 views

### Correctness proof of recursive-descent recognizer

Let G be a grammar that contains no left-recursive rules, and we use a recursive-descent recognizer that uses full backtracking, using list of results for example, to recognize strings of G. How ...
0answers
68 views

### Proof of convergence of alternative minimization/maximization [duplicate]

Given a problem $$\max_{x\in X} \min_{y \in Y} f(x,y)$$ where $f$ is strongly convex in $Y$ and strongly concave in $X$ How to show that the following iterative ...
1answer
355 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 ...
0answers
229 views

### Famous computer science results which correctness is uncertain?

I am asking the following: which of the 'famous' computer science results have been thoroughly checked, and for which ones is the correctness still uncertain? I understand that some proofs are hard ...
1answer
83 views

### The random densification technique-JL lemma

In Ailon's paper (p.3): How $1/(20nd)$ is obtained?
0answers
232 views

### Equational Logic and First Order Predicate Logic

I am interested in using Equational Theories (ET) together with Equational Logic (EL) found in algebraic specification languages such as CafeOBJ . I wish to use ET+EL to represent and prove sentences ...
0answers
80 views

### A self-contained proof that OrdHorn relations are tractable?

I'm currently investigating a family of temporal relations called 'Ordered Horn' ($OH$ for short). This class was introduced in 'Reasoning about Temporal Relations: A Maximal Tractable Subclass of ...
0answers
124 views

### Randomly Discovered Algorithm/Counterexample

I was reading Scott Aaronson's blog, and one of the comments sparked a question. "if P!=NP, this would be a general, conceptual result, so you’d expect the proof to be explanatory and in particular ...
1answer
154 views

### Proof-techniques for the hardness of optimization problems (esp. Polynomial time)

I've given an optimization problem for which I want to show that it is solvable in polynomial time. Now, I have two questions: Can this be done by formulating a mixed-integer linear program such ...
1answer
320 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 ...
1answer
235 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: ...
1answer
245 views

### Is it worthwhile to try to prove a conjecture by mapping it to a Turing machine?

Lets assume the proof of a conjecture, for example, the famous Goldbach conjecture. Is it possible to try to prove or disprove such a conjecture by devising a Turing machine that accepts if the proof ...
1answer
241 views

1answer
819 views

### Alternative Turing Machine Proofs

I am asking this question again. I am aware of, and have read the other similar "alternative proof TM" questions, but unfortunately, they do help me. I am looking for a TM Halting Problem proof that ...
2answers
1k views

### Is there an alternative proof of the TM Halting Problem other than the “standard” one? [closed]

I'm wondering if anyone is aware of a proof of the Halting Problem that is not just a permutation of the "standard" proof. Since there are so many formulations of this proof, rather than pick a ...
1answer
649 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 ...
4answers
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 ...
4answers
2k 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 ...