Skip to main content
89 votes
Accepted

What does it mean to suspect that two conjectures are logically equivalent?

First of all, in practice when we say "Conjecture A is equivalent to Conjecture B," what we mean is "We have a proof that Conjecture A is true iff Conjecture B is true." We can have such a proof ...
Noah Schweber's user avatar
73 votes

Replication crisis in mathematics

Mathematics does have its own version of the replicability problem, but for various reasons it is not as severe as in some scientific literature. A good example is the classification of finite simple ...
69 votes

What does it mean to suspect that two conjectures are logically equivalent?

Noah Schweber's answer is in some sense the "right" answer, and I would have said something similar if he hadn't beaten me to it. However, I think that it's worth pointing out that reverse ...
Timothy Chow's user avatar
  • 80.3k
51 votes
Accepted

"Strange" proofs of existence theorems

There are probabilistic proofs of existence. Do they fall into one of your three categories? For example, prove the existence of a real number that is normal in all bases: To do it, we show that "...
Gerald Edgar's user avatar
  • 40.6k
46 votes

What does it mean to suspect that two conjectures are logically equivalent?

One way to say rigorously what it means for two true theorems to be equivalent is to find a meaningful way to generalize both of them to statements that aren't always true, and then prove that they're ...
Qiaochu Yuan's user avatar
38 votes
Accepted

Did Euler prove theorems by example?

There's some evidence that precisely the opposite can be said: that Euler is aware of the fallacies of proving theorems by example (of course, this does not necessarily mean he has never used it). One ...
30 votes

Did Euler prove theorems by example?

"Proof by example" is a technique used by Euclid, who often proved results that hold e.g. for n integers in a typical case, say for 3 integers, as well as by Diophantus, who had to choose values for ...
27 votes

"Strange" proofs of existence theorems

There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$ is rational. The proof considers two cases: $\sqrt{2}^\sqrt{2}$ is irrational, or it is rational. In ...
Sam Hopkins's user avatar
  • 23.1k
27 votes
Accepted

How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

The simply-typed $\lambda$-calculus is not stronger than second-order logic. The simply-typed $\lambda$-calculus has: product types $A \times B$, with corresponding term formers (pairing and ...
Andrej Bauer's user avatar
  • 47.9k
26 votes

How is it possible for PA+¬Con(PA) to be consistent?

As is being discussed in the comments, the non-standard proofs in non-standard models of $\mathsf{PA}$ are not trustworthy (in that they're not sound). I'll give a sort of 'toy model' illustrating the ...
James E Hanson's user avatar
25 votes

Has Apéry's proof of the irrationality of $\zeta(3)$ ever been used to prove the irrationality of other constants?

Regarding your second question, Apéry's amazing formula $$\zeta(3) = {5\over 2} \sum_{n\ge1} {(-1)^{n-1} \over n^3 {2n \choose n}}$$ has inspired the search for analogous formulas for other zeta ...
Timothy Chow's user avatar
  • 80.3k
22 votes
Accepted

Has Apéry's proof of the irrationality of $\zeta(3)$ ever been used to prove the irrationality of other constants?

The proof of irrationality of $\displaystyle\sum_{n=0}^{+\infty}\frac1{F_n}$ (where $F_n$ is the $n$-th Fibonacci number) by RIchard André-Jeannin is an adaptation of the original Apery's proof of the ...
joaopa's user avatar
  • 3,811
21 votes

"Strange" proofs of existence theorems

This is the strangest existence proof I know; it is a nonconstructive proof that there exists a proof of a certain statement. In other words, we prove the statement by proving that a proof exists. I'...
Nik Weaver's user avatar
  • 42.4k
21 votes

What is the logical status of the sentence combining the ideas of Löb and Rosser, "this sentence is provable before any proof of its negation"?

As Akiva Weinberger conjectured, this depends on the implementation. Indeed, $0=0$ is a sentence of this type, i.e. $0=0$ is equivalent to the claim that there is a proof of $0=0$ that is shorter than ...
Will Sawin's user avatar
  • 141k
21 votes

Brute force open problems in graph theory

The existence of a 57-regular "Moore graph" is one such problem. We define the diameter of a graph $G$ to be the least $l$ such that any two vertices $u,v$ have a path between them using $\...
20 votes

The Halting Problem and Church's Thesis

The invocation of Church's thesis is not a religuous move but rather a warning to the reader that the author is describing informally an effective procedure which could be translated into a ...
Andrej Bauer's user avatar
  • 47.9k
17 votes

Has Apéry's proof of the irrationality of $\zeta(3)$ ever been used to prove the irrationality of other constants?

As Frits Beukers writes in http://www.staff.science.uu.nl/~beuke106/caen.pdf "Ironically all generalisations tried so far did not give any new interesting results. Only through a combination of ...
Zurab Silagadze's user avatar
16 votes

"Strange" proofs of existence theorems

Many existence proofs in analysis / probability follow this line of argument: 1. Construct a family of objects that approximately satisfy some desired property. 2. Show that the family is precompact. ...
Martin Hairer's user avatar
16 votes
Accepted

Status of proof by contradiction and excluded middle throughout the history of mathematics?

I want to echo the other answer, that Brouwer presents the first robust challenge to the Law of Excluded Middle (LEM), but I do want to add some history and background, and maybe recommend a related ...
Ben Burns's user avatar
  • 839
16 votes

Replication crisis in mathematics

How can we expect that increasingly complicated proofs are replicated when so few people can understand them in the first place? My answer to that is that we do not expect them to be replicated in the ...
16 votes

Brute force open problems in graph theory

Elaborating on the comment of Wojowu, for what positive integers $q$ does there exist a bipartite graph $G$ with vertex bipartition $(A,B)$ satisfying: (a) $|A|=|B|=q^2+q+1$, (b) $G$ is regular of ...
15 votes
Accepted

van der Waerden's theorem in Reverse Mathematics

There is a powerful combinatorial theorem, known as the Hales–Jewett theorem, which readily implies van der Waerden's theorem. On the other hand, the paper below by Matet exhibits primitive recursive ...
Ali Enayat's user avatar
  • 17.3k
15 votes

Replication crisis in mathematics

Has this crisis impacted (pure) mathematics, or do you believe that maths is mostly immune to it? Immune to the replication problem, yes. But not immune to the attitudes which cause scientists to do ...
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 ...
Sam Nead's user avatar
  • 27k
14 votes
Accepted

Let's keep adding once undecidable statements

Short answer: $ZFC_\alpha$ only makes sense for those $\alpha$ which have "nicely definable representations" - specifically, for the computable ordinals $\alpha$. (An ordinal is computable if there is ...
Noah Schweber's user avatar
14 votes

Is there good reference for proof complexity?

These are three books that I know: Logical Foundations of Proof Complexity Bounded Arithmetic, Propositional Logic and Complexity Theory Logical Foundations of Mathematics and Computational ...
Erfan Khaniki's user avatar
14 votes
Accepted

How can we know the well-foundedness of $\epsilon_0$?

Let me use the notation $\omega_n$ for an exponential tower of $\omega$'s of height $n$, so $\omega_{n+1}=\omega^{\omega_n}$. Then $\epsilon_0$ is the supremum of $\{\omega_n:n\in\omega\}$. PA proves ...
Andreas Blass's user avatar
13 votes
Accepted

The Halting Problem and Church's Thesis

Let me point out that there are really a family of Church-Turing theses assertions. On the one hand, for what is sometimes described as the weak Church-Turing thesis, one imagines an idealized human ...
Joel David Hamkins's user avatar
13 votes
Accepted

Cut-free proofs in ZFC

Yes, one can eliminate cuts polynomially for proofs in ZFC, PA, and similar theories that have nontrivial axiom schemata allowing arbitrary formulas. For PA, replace a cut $$\color{blue}{\dfrac{\...
Emil Jeřábek's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible