Two (probably) equal real numbers which are not proved to be equal?

Can someone give me a nice example of two computable real numbers which are believed but not proved to be equal?

I never really understood the assertion that "the reals do not have decidable equality" until I saw concrete examples such as this gem. It's clear that both sides are well-defined real numbers, however it's not at all clear how one might go about proving their equality. However, perhaps a little disappointingly, on page 10 of this article by Bailey, Borwein, Broadhust and Zudilin, the equality is proved (and that article appeared on ArXiv before Stanley's post).

It's very easy to give "silly" examples of real numbers which are probably equal but not provably equal, e.g. the real number which is 0 if the Birch and Swinnerton-Dyer conjecture is true and 1 if not, is probably equal to zero, but we can't prove it. So for the pedants, can anyone give me an example of two computable real numbers whose equality is believed, but not known? More informally, I am looking for an example like the one Richard Stanley mentions in the link above where computer scientists can compute both sides to a gazillion decimal places but mathematicians can't prove equality rigorously? Stanley calls such things rare. Several potential examples are mentioned on p13 of the BBBZ paper I cited above, however that paper was written ten years ago and things seem to move fast in this area. Are any of these still open? It looks to me like the authors are developing techniques which might solve them. For example equation (10): if

$$Cl_2(\theta):=-\int_0^\theta\log|2\sin(\sigma)|d\sigma$$

and $$\theta_2:=2\tan^{-1}(\sqrt{2})$$ then is

$$27Cl_2(\theta_2)−9Cl_2(2\theta_2) + Cl_2(3\theta_2)= 8Cl_2(\pi/4)+ 8Cl_2(3\pi/4)$$ still an open problem?

• Example 1, example 2, example 3. All identities involve computable numbers and are equivalent to RH. – Wojowu May 7 at 15:16
• As much as I like the question, I feel like it would fit better on Math.SE. – Wojowu May 7 at 15:20
• As one of the pedants mentioned in the last paragraph of the question, I must point out that "0 if the Birch and Swinnerton-Dyer conjecture is true and 1 if not" is a computable real number. Admittedly, we don't know which of two obvious algorithms computes it, but we (using classical logic) do know that there exists an algorithm computing it, and that's what "computable" means. – Andreas Blass May 7 at 17:17
• You can take an elliptic curve over ${\mathbb Q}$ with rank 4. Then the second derivative of its L-function at s=1 is computable (if you start from a twist of $y^2=x^3-x$, you can even write an explicit series), should be 0, but no one knows how to prove it. – Zidane May 7 at 21:00
• The article en.wikipedia.org/wiki/Experimental_mathematics has some nice true, false, and unsolved examples. $\sum_{k=1}^\infty \frac{1}{k^2}\left(1+\frac{1}{2}+\frac{1}{3}+\cdots+\frac{1}{k}\right)^2 = \frac{17\pi^4}{360}$ was verified to 100+ decimal digits (see reference linked from the wiki page) but might still be unproven. – none May 8 at 6:47

As mentioned in another MO question, Gourevitch's conjecture is a nice example: $$\sum_{n=0}^\infty \frac{1+14n+76n^2+168n^3}{2^{20n}}\binom{2n}{n}^7 = \frac{32}{\pi^3}.$$

• This is verified numerically with Mathematica, although I can’t coax it to give me the exact answer ... I think this should be possible, let’s see ... – EGME May 12 at 19:17
• While I let the computer run and trying something, I can add that you can compute equality to any number of digits you want. M does produce an exact solution for the summation, but it doesn’t “know” (at least not yet) that it is identical to the RHS of the above. Let’s see what happens if I let this run for a while. – EGME May 12 at 19:45
• Oh this one would be perfect! Is it still open? – Kevin Buzzard May 12 at 20:10
• @KevinBuzzard J. Guillera confims that this is an open problem today (13 may 2019). I haven’t discounted the possibility of doing it with Mathematica just yet. – EGME May 13 at 16:41
• @KevinBuzzard : It occurs to me that Gourevitch's conjecture, nice though it is, may not be a convincing example if you're trying to wrap your head around things such as Richardson's theorem. I believe that it is known how to decide Gourevitch's conjecture on a sufficiently powerful computer, and the problem is that current computers aren't powerful enough. I think the key to Richardson's theorem is that you can use trig functions to simulate arbitrary Diophantine equations and then invoke the negative solution to Hilbert's 10th problem. – Timothy Chow Jul 29 at 13:49

Thomson’s problem for $$n = 7$$ provides a nice example:

$$\min_{x_1, \ldots, x_7 \in \mathbb{S}^2} \sum_{i=1}^7 \sum_{j = i + 1}^7 \frac{1}{|x_i - x_j|} = \frac{1}{2} + 10 \frac{1}{\sqrt{2}} + 5\sqrt{\frac{2}{5 + \sqrt{5}}} + 5\sqrt{\frac{1 + \sqrt{5}}{2\sqrt{5}}}$$

Now let me explain. Thomson's problem is to find the minimal energy configuration for $$n$$ electrons on a unit sphere, i.e. the left-hand-side of the equation. The answer is only rigorously known for $$n \leq 6$$ and $$n = 12$$. For $$n = 7$$ the solution is only conjectured.

Now, the left-hand side of the equation above is computable since it is the minimum of a computable function over the sphere. (Moreover, it is fairly efficient to compute in practice, hence the filled-in table of minimal energies in the Wikipedia article.)

The right hand side is the energy of the conjectured optimal configuration for the $$n=7$$ case. (See here for the specific distances between points, which I used in the above equation.)

Many of the other values of $$n$$ have conjectured solutions and therefore give rise to similar equations.

One thing which I find crazy about this example (and which might ruin it for you), is that while this equation has never been rigorously proved, it’s truth/falsity is decidable by the decidability of real-closed fields (see my answer to a similar problem here). Hence a clever programmer-mathematician may find a computer-assisted rigorous proof. Indeed, this is exactly what happened for the $$n=5$$ case. (Schwartz used custom code. It would be nice to have someone redo this computation in a formal theorem prover like HOL Light, Coq, or Lean.)

• After breaking the symmetry (by fixing one electron and the direction to another that is not antipodal), the set of critical points is the intersection of some algebraic surfaces and is almost certainly provably finite using Groebner basis methods, although the computations may be too difficult to be practical. – Robert Israel May 8 at 3:11
• An open conjecture in arithmetic geometry is whether any group scheme of order n is killed by n. This is true for n=1 and n prime (the latter a theorem of Deligne) but the n=4 case is still open. The n=4 case is simply the question "here is a completely explicit polynomial ring over the integers in about 20 variables -- is this explicit element in this explicit ideal?". Groebner basis methods are apparently not up to this yet. – Kevin Buzzard May 8 at 8:31
• Just to be clear -- the n on the left hand side of the equation in this answer is 7, right? – Kevin Buzzard May 8 at 8:31
• @KevinBuzzard Yes, $n=7$. I’ve made it explicit now. – Jason Rute May 8 at 10:58
• The "min" annoys me a bit in this example, for some reason I can't quite explain. – Kevin Buzzard May 11 at 15:34

The conjectures on special values of $$L$$-functions provide a lot of examples. For example, David Boyd conjectured in his celebrated paper that the Mahler measure of the Laurent polynomial $$P_k(x,y)=x+\frac{1}{x}+y+\frac{1}{y}+k$$, where $$k$$ is an integer $$\neq 0, \pm 4$$, is proportional to $$L'(E_k,0)$$, where $$E_k$$ is the elliptic curve defined by the equation $$P_k(x,y)=0$$. It is not difficult to check these identities numerically to thousands of decimal places, but so far they have been proved only in a finite (and small) number of cases. (Technically you asked about equalities, here they involve some rational factor, which is however simple enough to guess in each particular case, although its value in general is mysterious, e.g. may be linked to the Bloch-Kato conjectures).

The equality mentioned in the OP (page 10 of Bailey-Borwein-Broadhurst-Zudilin) is essentially Borel's theorem in disguise for the $$K$$-group $$K_3(\mathbb{Q}(\sqrt{-7}))$$. Equation (10) of the same article is an instance of the following question: we have two elements in some $$K$$-group which has (or should have) rank 1, so they should be proportional hence their regulators should also be proportional. In the present case, equation (10) should follow from the 5-term functional equation of the dilogarithm evaluated at particular algebraic arguments, which is however not an easy task (there is an obvious but inefficient algorithm since the set of algebraic numbers is countable).

The moving sofa constant is conjectured to be 2.2195..., which is computable as the implicit solution of a set of equations (see Eqs. 1-4 in Romik 2018). On the other hand, while not immediately obvious, the fact that the moving sofa constant is computable is reasonably intuitive, and in fact, Dan Romik and I proved that it is.

Consider $$x = \sum_{n=0}^\infty a_n 2^{-n}$$ where $$a_n = 1$$ if $$n$$ is an odd perfect number, $$0$$ if not. It is suspected that $$x = 0$$, but not known. By checking the first $$n$$ natural numbers, we can approximate $$x$$ with an error at most $$2^{-n}$$.

Along similar lines: by the solution to Hilbert's 10th problem a polynomial $$P(a, x_1,\ldots,x_n)$$ with integer coefficients is known explicitly, such that the set of natural numbers $$a$$ for which $$P(a,x_1,\ldots,x_n)=0$$ has a solution in natural numbers is not computable. Of course if such a solution exists, we can compute that it exists, but there is no algorithm to decide whether it exists. Let $$X(a) = \sum_{(x_1,x_2,\ldots,x_n) \in \mathbb N^n} \chi_0(P(a,x_1,\ldots,x_n))\; 2^{-x_1 - \ldots - x_n}$$ where $$\chi_0(x) = 1$$ if $$x=0$$, $$0$$ otherwise. The numbers $$X(a)$$ are all computable in the sense that arbitrarily good approximations are available, but there is no algorithm to decide whether $$X(a)=0$$. For any consistent theory $$T$$, there are some $$a$$ such that $$X(a)=0$$ but there is no proof in $$T$$ that $$X(a)=0$$.

• I am irritated that (a) I cannot understand equation (10) in BBBZ and (b) all the other answers have been of the form "let's encode a well-known conjecture into a possibly slightly artificial real number". The original now-proved equality had none of these deficits. – Kevin Buzzard May 7 at 19:21

One of my favourite answers to this question is due to @Zidane, who wrote it as a comment to the question.

Let $$E$$ be an elliptic curve of algebraic rank 4, for example the curve

$$y^2 + xy = x^3 − x^2 − 79x + 289$$

(see for example equation 1.4.1 of William Stein's book). The current state of the art (as far as I know) is that BSD says that this curve should have analytic rank 4, however known techniques cannot rule out analytic rank 2. Hence $$L''(E,1)$$ is conjectured, but not known, to be zero. The curve is modular, and the $$L$$-function of the modular form can be analytically continued to $$s=1$$ no problem, and its second derivative computed to many decimal places. My memory is that Stein did in fact do this, and observed that, unsurprisingly, it looked like it was zero. I guess it would actually be a big breakthrough if this number were proved to be zero; we don't as far as I know have techniques which access second derivatives of $$L$$-functions of elliptic curves yet.

For a very long time, people believed but could not prove that the densest possible sphere packing had density $$\pi\over 3\sqrt 2$$.

This was Kepler's conjecture, finally proved by Hales in 1998, or alternatively (since the referees reported that they were 99% sure that the 1998 proof was correct but they couldn't be completely sure), by Hales and collaborators through machine formalization completed in 2015.

• It's kind of annoying that this is an example of the form "These numbers were conjectured to be equal...oh but now it's a theorem". This answer hence suffers from the same problem which Stanley's post does. Your 17 pi^4/360 comment has none of these problems -- please post that as an answer too! – Kevin Buzzard May 8 at 8:37
• @Wojowu while it's definitely not clear that the optimal sphere packing density is computable, it's woth pointing out that the optimal lattice sphere packing is computable (Voronoi's algorithm), unproved for $n\ge 9$ ($n\neq 24$), and unlikely to be greater than known lower bounds for $9\le n\le 23$. – Yoav Kallus May 8 at 13:18
• As for whether the optimal sphere packing number is computable (before Hale’s proof), there has been a lot of confusion about this. I’ve heard highly qualified logicians say that Kepler’s conjecture is decidable from basically the decidability of RCF. Then similar ideas can be used to compute the optimal ratio. This appears not to be the case: mathoverflow.net/questions/317692/… (However the optimal packing in a cube of fixed size is computable. The issue is that the limit as the cube grows is not obviously computable.) – Jason Rute May 8 at 13:50
• @JasonRute that is really interesting about the limit as the cube grows: it sounds computable but it might not be, if it converges slowly enough that the cube has to grow by an uncomputable amount for each extra decimal place. I wonder if there are interesting mathematical constants that can be described as straightforward infinite series but are uncomputable for that reason. I don't count things like Chaitin's constant. – none May 9 at 9:15
• I think optimal density in cube should approximate optimal density in Euclidean space to constant/(cube side): from above, tile the cube to get an infinite packing; from below, pick cubic region of the infinite packing with highest density and remove the balls that stick out. So, the optimal packing should be computable, but Henry Cohn's answer linked above is about decidability of eaulity to a certain value, which is a different issue. – Yoav Kallus May 10 at 1:52