Theorems that are essentially impossible to guess by empirical observation There are many mathematical statements that, despite being supported by a massive amount of data, are currently unproven. A well-known example is the Goldbach conjecture, which has been shown to hold for all even integers up to $10^{18}$, but which is still, indeed, a conjecture.
This question asks about examples of mathematical statements of the opposite kind, that is, statements that have been proved true (thus, theorems) but that have almost no data supporting them or, in other words, that are essentially impossible to guess by empirical observation.
A first example is the Erdős–Kac theorem, which, informally, says that an appropriate normalization of the number of distinct prime factors of a positive integer converges to the standard normal distribution. However, convergence is so slow that testing it numerically is hopeless, especially because it would require to factorize many extremely large numbers.
Examples should be theorems for which a concept of "empirical observation" makes sense. Therefore, for instance, theorems dealing with uncomputable structures are (trivially) excluded.
 A: In 1912 Sergei Bernstein studied the best uniform approximation of $|x|$ on
$[-1,1]$ by polynomials of degree $2n$. Denoting $E_{2n}$ the error
of the best approximation, he proved the existence of the limit
$$\beta=\lim_{n\to\infty}2nE_{2n}.$$
This number is called the Bernstein constant nowadays. His own numerical estimation gave $0.278<\beta<0.286$; noting that these estimates have an average of $0.282$, which is very close to $(2\sqrt{\pi})^{-1}$, Bernstein conjectured that
$\beta=(2\sqrt{\pi})^{-1}$.
This was disproved in a 1985 paper by Richard Varga and Amos Carpenter, who computed $\beta$ to fifty decimal places, and proved bounds tight enough to determine the first four digits as $0.2801$. Their result disagrees with Bernstein's conjecture already in the third digit. Nothing is known about the arithmetic nature of $\beta$.
A: One of the most interesting examples that happened recently is the Katz-Sarnak conjecture asserting that the average rank of elliptic curves (ordered by some reasonable height) defined over $\mathbb{Q}$ is equal to $1/2$. This is a generalization of a more specific conjecture due to Goldfeld which asserts that the average rank of quadratic twists of a given elliptic curve is equal to $1/2$. Goldfeld's conjecture dates back to the 1970's and the Katz-Sarnak conjecture was made in the 1990's.
This is a story that was told by Manjul Bhargava during one of his lectures at Oxford where I was in the audience. He said that, as a graduate student at Princeton in the 90's, he had heard Sarnak lecture on his conjecture with Katz. Curious, Bhargava then looked up existing data on the average rank of elliptic curves and found that of the tens of thousands of elliptic curves that were tabulated, the average rank was quite large (exceeding two), and appeared to be increasing. The young Bhargava printed out the results and showed Sarnak the next day, stating that the data clearly does not support his conjecture. According to Bhargava, without batting an eye Sarnak said "the data is misleading; eventually the average rank will plateau and start going down towards $1/2$ when more curves are considered". Bhargava was apparently unconvinced.
The story of course eventually leads to the groundbreaking work of Bhargava and Arul Shankar in the last decade on average rank of elliptic curves. In three spectacular papers(here, here, and here) they proved that the average rank of elliptic curves, sorted by the "naive height" defined for an elliptic curve given in short Weierstrass form $E_{A,B} : y^2 = x^3 + Ax + B, A,B \in \mathbb{Z}$ as $H(E_{A,B}) = \max\{4|A|^3, 27B^2\}$, is at most $1.5, 1.17, 0.885$ respectively. The lecture mentioned above was given in 2016. At the time, the existing data had not yet shown that the average rank dips below 1, even though the best theoretical result gives an upper bound of $0.885$. Bhargava ended his talk by displaying a brand new chart showing that the average rank seems to dip below $0.9$, still above the theoretical bound, compiled by the work of his students and collaborators.
A: Bootstrap percolation is a two-dimensional two-state cellular automaton with a von Neumann 5-square ("plus") neighborhood where a "white" cell become "black" if it has at least 2 black neighbors, and a black cell always remain black.

The question is: on a $L \times L$ square, how dense should the (uniformly random) initial population be to make the whole square black? The result is determined by the critical value $\lambda=\pi^2 /18 \approx 0.548$. When the initial density $p$ satisfies $p \log(L) > \lambda$, the final population will be entirely black with high probability, and if $p \log(L) < \lambda$, the final population will contain white cells with high probability.
Simulations in this paper used $L=28800$ and suggested a critical value of $\lambda = 0.245 ± 0.015$. According to this webpage, to get close to the limiting value, one needs $L$ at least $10^{20}$, certainly well beyond the range of any computer!
A: Other answers mention some advanced math theorems that are mostly beyond my understanding. But the fact that the sum of inverse of the prime numbers diverges still baffles me. I have seen no intuition or empirical data to support it (which might be due to my limited knowledge). Euler's proof and a few other ones that I've read were solely based on abstract mathematical facts, contrary to the infinitude of sum of harmonic numbers which had some nice intuitive proofs.
A: The following approximation to $\pi$, from "Strange Series and High Precision Fraud" by Borwein and Borwein, provides another example:
$$ p:=\left(\frac1{10^5} \sum_{n=-\infty}^\infty e^{-\frac{n^2}{10^{10}}} \right)^2 \approx \pi,$$
where the left and the right side agree for at least 42 billion decimals.
Certainly, the theorem "$p \neq \pi$" could not have been found empirically!
A: Letting $\pi$ be the prime counting function and $\mathrm{Li}$ the logarithmic integral, Littlewood proved in his 1914 article "Sur la distribution des nombres premiers" that the difference $\pi(x)-\mathrm{Li}(x)$ changes sign infinitely many times; however, according to Wolfram Math World: Skewes Number, Kotnik proved that the smallest number for which this happens is greater than $10^{14}$.
A: Recent breakthrough work of Ben Green together with an improvement by Zach Hunter imply that there is a red-blue coloring of $[1,n]$ with no red $3$-term progression and no blue $k$-term progression for $$n = k ^{ \frac{ c \log k }{\log \log k }}.$$
On the other hand, empirical observation suggests this is only possible for $n \approx k^2$.
Moreover the proof is, as far as I know, constructive, i.e. it gives a randomized algorithm to produce an example with high probability. It's just that this algorithm needs relatively large $n$ to do better than $k^2$.
A: Going back to the 18th century, when L. Euler established $$\sum_{n\ge1}\frac1{n^2}=\frac{\pi^2}6,$$
he certainly had no guess about the value from empirical observation (= partial sums).
A: A slightly old question, but I've only just seen it...
Lord Brouncker proved in 1654 that
$$
\dfrac{1}{4}\pi
=
\cfrac{1}{1+\cfrac{1^2}{3+\cfrac{2^2}{5+\cfrac{3^2}{7+\dotsb}}}}
$$
This has very slow convergence. Apparently people didn't believe it initially. It takes nearly 50 terms for five decimal places of accuracy and nearly 120 for six! It converges in an oscillatory manner and the jumps are quite large for quite a long time.
Of course, 120 terms isn't that many for modern computers and there would be no doubt about it these days. But, 120 is a lot to do by hand in the 1650s!
A: Goodstein's theorem. For a nonnegative integer $n$, the hereditary base $b$ representation of $n$ is found by writing $n$ in base $b$, then writing the exponents in base $b$, recursively, until the process terminates when all exponents are less than $b$. For example, the hereditary base $3$ representation of $59056$ is $3^{3^2 + 1} + 2 \cdot 3 + 1$.
Now for a positive integer $k$, we can define the Goodstein sequence $G_k$ by $G_k(0) = k$, and obtain $G_k(n+1)$ from $G_k(n)$ by writing $G_k(n)$ in hereditary base $n+2$, replacing each instance of $n+2$ with $n+3$, and then subtracting one.
Goodstein's theorem states that these sequences always reach $0$. However, for $k \ge 4$, it takes an extremely large number of iterations for this to occur, or even for the terms to start decreasing. (It is claimed on Wikipedia that, for $k=4$, the terms increase until base $3 \cdot 2^{402\ 653\ 209}$.) This makes the theorem effectively impossible to discover by empirical observation.
A: Khinchin's constant is a good one: https://en.m.wikipedia.org/wiki/Khinchin%27s_constant
It says that for almost all real numbers, the limit of the geometric mean of the first $n$ coefficients of their continued fraction expansion converges as $n$ goes to infinity. Not only does it converge, it converges almost always to the same value  - Khinchin's constant - independent of the number you started off with.
I'm not up to date on any new results on this, but it seems that this property has only been shown to hold for numbers that were constructed for this property to hold. Numerical evidence suggests that $\pi$, $\gamma$ and Khinchin's constant itself satisfy this property.
A: Probably Shannon's theorem(s) about existence of good (error-correcting) codes is an example: "most"/"random" codes achieve close to channel capacity, but explicit description (and economical decoding algorithms) has been a major research problem for the intervening decades.
This example seems especially piquant to me, because we want a code that is "random" enough to be good, but "secretly" structured in human/algorithmic terms that we can efficiently compute with it.
A: Fast-growing functions provide one source of examples. Here is one that Harvey Friedman has described in his paper on Long finite sequences (J. Combin. Theory Ser. A 95 (2001), 102–144; see also his lecture notes on Enormous Integers).

Say that a ternary sequence $x_1, x_2,\ldots, x_n$ is block subsequence free if for no $i < j \le n/2$ is $x_i,\ldots,x_{2i}$ a subsequence of $x_j,\ldots, x_{2j}$.  Are there arbitrarily long block subsequence free ternary sequences?

The answer is no. But to write down the maximum length of such a sequence, you need the Ackermann function (or some similar notation).  That is, if you empirically try to write down a long block subsequence free ternary sequence, all the evidence will suggest that you can continue forever.
A: So-called non-constructive proofs in combinatorics typically yield existence proofs of certain combinatorial objects without providing any efficient algorithm for finding them. These proofs may rely on counting arguments or on algebraic or topological existence results that have no known efficient algorithm.  Paradoxically, the proofs sometimes guarantee the existence of exponentially many objects, yet fail to provide an efficient method of finding even one. Howard Karloff has described such situations as "finding hay in a haystack."
You can find many examples in this paper by Noga Alon, such as the following result of J. Spencer.

Let $v_1,\ldots,v_n$ be $n$ real vectors of length $n$ each, and suppose that the $\ell^\infty$-norm
of each $v_i$ is at most $1$. Then there are $\epsilon_1,\ldots,\epsilon_n \in \{−1,1\}$ such that the $\ell^\infty$-norm of the sum
$\sum_{i=1}^n \epsilon_i v_i$ is at most $6\sqrt{n}$.

I believe that if you were to investigate this question empirically by generating examples and computationally searching for suitable signs, you would soon encounter instances for which you would be unable (in practice) to achieve the bound guaranteed by Spencer's theorem.  Alon speculates that there should exist an efficient algorithm, but as of the time he wrote the paper, no such algorithm was known. [EDIT: This is probably not the best example from Alon's paper to illustrate the point I'm making; see comments below.  The Lovász Local Lemma gives better examples; e.g., a $k$-uniform hypergraph in which each edge shares vertices with at most $\sim 2^k\!/e$ other edges admits a 2-coloring with no monochromatic edge, but I doubt that this theorem would have been found empirically. There is now a polynomial time algorithm for finding the coloring, but it is highly sophisticated, and the search for such an algorithm was motivated by the theorem, rather than the other way around.  See also this blog post by David Eppstein which summarizes a talk by Noga Alon on this topic.]
In a similar vein, Keevash's spectacular proof of the existence of designs allows us to write down parameters for combinatorial designs which we now know must exist, even though we can't write down explicit examples. Empirical search for such designs would of course turn up empty.
A: The growth rate of $n\mapsto\mathrm{TREE}(n)$ seems to be impossible to guess from experiments or observation
A: Pretty much every proof in computability theory using a priority construction could be said to have this property since, if you work through them virtually every substantial step  operates on some initial segment that's far too long to practicly check (eg you'll be trying to preserve an initial segment long enough to let the first n computable functionals converge if they ever do so at any point in the construction with interesting n being pretty big...not quite busybeaver see that kind the thing).
Note the computability results are usually the kind of results that one should be able to in principle get empirical support for (eg, they make a claim that all naturals have/fail some checkable property or that there is an e such that all  s has some checkable property or, most often, a Pi-0-3 property).
For instance, the claim that there is an incompatible pair of re degrees is a claim of the form $\exists e, i \forall j \exists n$ but since all the important action happens at hugely large values of $n$ you couldn't hope to gain meaningful direct empirical support even given the values of e, i that work.  I'm sure there is a better example of a $\Pi^0_2$ claim proved via a priority argument but it's not popping out at me now.
