54
votes
Techniques for debugging proofs
Several basic suggestions.
First, put your manuscript into a drawer, and forget about it for a couple of months. You will discover a whole lot of exciting new things when you take it off from the ...
39
votes
Techniques for debugging proofs
I find that there is a surprisingly large class of proofs for which it is possible to write software representations of many ingredients. I usually use Maple, but of course there are other options. ...
32
votes
Techniques for debugging proofs
When I was an undergraduate student, one of my professors used to repeat during classes: “this is obviously true - let’s see if it’s also true”.
Recalling those words proved useful many times, so here’...
26
votes
Techniques for debugging proofs
When writing a long paper (~100 pages) with many long chains of equalities and inequalities a few years ago, I developed a system of LaTeX macros that make a semantic distinction between “definitional”...
18
votes
Techniques for debugging proofs
There are two important classes of proofs not explicitly mentioned in other answers -
Where the theorem is correct in all cases of interest, but not strictly correct as stated;
Where the theorem is ...
15
votes
Computational complexity theoretic incompleteness: is that a thing?
Consider the sentence $P(n)$ which says "This sentence has no proof shorter than $n$ characters." This sentence is true, and even has a proof - enumerate all strings of length $n$ and check ...
- 28.2k
12
votes
Accepted
What exactly is a judgement?
I highly recommend reading Martin-Löf's paper referenced by Ulrik Buchholtz in the comments to your question. Apart from that, here are a couple of point that might help, some of which were already ...
- 48.8k
11
votes
How does proof assistant organize knowledge?
Organization of mathematics in computerized form is a somewhat separate topic from automated and assisted theorem proving. Here are some pointers that will get you started:
MathWebSearch, a content-...
- 48.8k
10
votes
Accepted
Computational complexity theoretic incompleteness: is that a thing?
Yes, this sort of thing has been considered before, for example by Harvey Friedman and Pavel Pudlák. Here is a representative result. If we let $\mathsf{Con}(\mathsf{PA},n)$ denote the statement that ...
- 82.7k
9
votes
What exactly is a judgement?
I think the problem here is that different logical systems can formalize different sorts of information. For example, in traditional deductive systems, the notion of "well-formed formula" is not ...
- 73.2k
8
votes
Accepted
Are there any recent advances in formalizing the undecidability of $\mathit{CH}$?
Jesse Michael Han and Floris van Doorn recently formalized the independence of the continuum hypothesis in the Lean theorem prover. See the Flypitch project webpage for their papers and code.
- 13.6k
7
votes
Accepted
Can we have consistent theories stating opposing provability statements that are non-standardly coded?
This idea in play here is due to Rosser and is the main idea behind the Gödel-Rosser theorem.
Specifically, Rosser proposes to consider the sentence $\rho$ asserting that for every proof of $\rho$ in ...
- 236k
7
votes
Computational complexity theoretic incompleteness: is that a thing?
This might be more of an analogy, but major complexity conjectures like P=NP could be considered related.
Background: a common "complete" problem for a specified time limit is: given a ...
- 4,529
7
votes
Computational complexity theoretic incompleteness: is that a thing?
These self-referential decision problems are already part of the subject of computational complexity. There are analogues of the halting problem, for example, for many of the various classes in the ...
- 236k
7
votes
Techniques for debugging proofs
Explain the proof to your cat. Indeed, it is often difficult to find a willing collegue listening for hours to all details without falling asleep or getting lost (both things happen simultaneously ...
7
votes
Binomial ID $\sum_{k=m}^p(-1)^{k+m}\binom{k}{m}\binom{n+p+1}{n+k+1}=\binom{n+p-m}{n}$
I wish to explain a modern (high tech) method called the Wilf-Zeilberger (WZ) technique which might help you (and anyone interested) with the present question and many others you encounter in the ...
- 43.2k
7
votes
Binomial ID $\sum_{k=m}^p(-1)^{k+m}\binom{k}{m}\binom{n+p+1}{n+k+1}=\binom{n+p-m}{n}$
It's a generating-function exercise. We have
$$
\sum_{k=m}^\infty (-1)^{k+m} {k \choose m} x^{k-m} = (1+x)^{-(m+1)},
$$
and (with $j=p-k$)
$$
\sum_{j=0}^\infty {n+p+1 \choose n+(p-j)+1} x^j
= \sum_{j=...
- 79.9k
6
votes
How true are theorems proved by Coq?
I just learned about the part of the Coq FAQ titled What do I have to trust when I see a proof checked by Coq?. To quote from the Apr 24, 2018 revision:
You have to trust:
The theory behind ...
- 35.5k
6
votes
Why we need to choose direction in the "marry the arrows" algorithm?
This exact point was discussed in that paper few paragraph before your quote:
Imagine for a moment that the strings of arrows represent streets—
circular drives, in the case of necklaces, and long ...
- 1,676
6
votes
Accepted
Proving that $P($$\{\text{$a$ and $b$ are co-prime}$ }$)=0$ for $a,b$ following the Uniform distribution over $[n, 2n]$ as $n \rightarrow \infty$
I seem to get the probability is still the usual $1/\zeta(2)$ by the usual inclusion/exclusion argument, but possibly there's a mistake in the following calculation:
$$
\begin{aligned}
\frac{1}{n^2}\...
- 47.4k
5
votes
Minimal Turing machines associated to math statements
For any statement S, there is some Turing machine T such that T halts iff S is true. If S is true, pick for T any Turing machine which halts. If S is false, pick for T any Turing machine which does ...
- 5,827
5
votes
Accepted
Binomial ID $\sum_{k=m}^p(-1)^{k+m}\binom{k}{m}\binom{n+p+1}{n+k+1}=\binom{n+p-m}{n}$
Such identities are often reduced to the Chu--Vandermonde's identity $\sum_{i+j=\ell} \binom{x}i\binom{y}j=\binom{x+y}\ell$ by using reflection formulae $\binom{x}k=\binom{x}{x-k}$, $\binom{x}k=(-1)^k\...
- 109k
4
votes
How does proof assistant organize knowledge?
Of course a hard part is to know whether two similar-looking lemmas are really related, and even more whether two superficially very different statements might have a short proof of their equivalence. ...
- 24.8k
4
votes
Accepted
Conjecture on minimum size of graph
We prove that, indeed, whenever graph $G=(V,E)$ is $n$-colorable and has less than $2(n-1)^2$ edges, it has 1-improper $(n-1)$-coloring.
Induction by $n$, base $n=1$, $n=2$ is clear. So we assume that ...
- 109k
4
votes
Accepted
How to use Meredith’s axiom for classical logic?
See https://us.metamath.org/mpeuni/meredith.html and the links there for the proofs you want.
- 39.9k
3
votes
Accepted
$\frac {f (0)}{2}+ \sum_{k=1}^{\infty}f (k)=\sum_{n=-\infty}^{\infty} \mathcal{L} \{ f \} (2 \pi i n)$
This is an answer to the question as it was originally formulated, it has now been heavily edited.
I consider this formula in the OP,
$$\sum_{k=1}^{\infty} f (k) = \int_{0}^{\infty}f(t)dt+ \sum_{n=...
- 188k
2
votes
Conjecture on minimum size of graph
Let us prove that any graph with $\chi_1(G)>n$ has at least $2n^2$ edges (with no assumptions on $\chi(G)$). This provides a sharp estimate (and the method also shows how to construct an optimal ...
- 23.7k
2
votes
Accepted
Extending a first-order deductive system with satisfaction relation
Given that your proof system includes ZFC, the standard way to handle algebraic structure like this in a set-theoretic context is simply to interpret those concepts in set theory. In the language of ...
- 236k
2
votes
Techniques for debugging proofs
Another technique that seems no one pointed is to explain your article to a colleague or a friend in details, and in his side will play the role of contradictor and double checker.
This trick is ...
1
vote
Techniques for debugging proofs
Check that you name things consistently. If in one chapter/lemma an index is denoted by $n$ and another index by $m$, and somewhere else it is the other way around, it can at best lead to unreadable ...
Only top scored, non community-wiki answers of a minimum length are eligible