57

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?

Kevin Buzzard
  • 40,559
  • I tried computing both sides using pari-gp but I've never used it for numerical integration before, and pari suggested that the right hand side was zero and the left hand side was about -10 :-( – Kevin Buzzard May 07 '19 at 15:02
  • 10
    Example 1, example 2, example 3. All identities involve computable numbers and are equivalent to RH. – Wojowu May 07 '19 at 15:16
  • 5
    As much as I like the question, I feel like it would fit better on Math.SE. – Wojowu May 07 '19 at 15:20
  • 1
    I know of rational quantities related to algebraic curves that were originally recognized by their decimal expansions through analytic methods and where later computed/proven by explicitly constructing the prime factorizations. Cf: https://arxiv.org/abs/0711.4316 – Aeryk May 07 '19 at 15:50
  • Hi Kevin, Mathematica gives a negligibly large number, practically 0, on both sides with numerical integrate. It has trouble with $3\pi/4$ in the fifth term so I made that 2.9999 ... It computes the RHS exactly as 0, and it produces a complex number with exact integration for the left hand side which is nowhere near 0. I will try to see if I can get something better for the LHS, I can use M pretty well. Pity about the discouraging comment ... I haven’t tried the latest version, will also do that ... – EGME May 07 '19 at 16:16
  • I stand corrected. The numerical integration produces, for the LHS, something not close to 0. I read my result incorrectly (need reading glasses) ... – EGME May 07 '19 at 16:43
  • https://rextester.com/KMHKJ81925 will execute the following R code, which gets LHS ~ 11 and RHS ~ 0: f <- function(s){log(abs(2sin(s)))}; Cl2 <- function(t){stats::integrate(f,0,t,abs.tol=1e-6)$value}; t2 <- 2atan(sqrt(2)); lhs <- 27Cl2(t2) - 9Cl2(2t2) + Cl2(3t2); rhs <- 8Cl2(pi/4) + 8Cl2(3*pi/4); c(lhs,rhs) –  May 07 '19 at 16:47
  • The LHS around -11 seems consistent with what I found ... – EGME May 07 '19 at 16:57
  • 13
    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 07 '19 at 17:17
  • 1
    @Wojowu inspired by your links one could even suggest $\Sigma_z|z|^{-100}$ where the sum is over all non-trivial zeros of $\zeta(s)$ which are not on the critical line :-/ Whilst I admit that this might well satisfy the requirements, it's somehow not what I was after :-/ – Kevin Buzzard May 07 '19 at 18:30
  • @AndreasBlass can you tell me how to rephrase the question to make it conform better to the meaning that I want to give it? – Kevin Buzzard May 07 '19 at 18:32
  • PS @Wojowu I am completely happy to move the question to Math.SE (but don't know how to); I no longer have a good feeling as to what belongs where and am happy to trust yours. – Kevin Buzzard May 07 '19 at 18:33
  • 5
    @KevinBuzzard Probably the best way is to just require that we know (and can prove) what algorithms compute the two numbers. Essentially equivalent: ask people to give you an example of two algorithms such that both are known to compute real numbers and those two real numbers are believed but not known to be equal. – Andreas Blass May 07 '19 at 18:48
  • 1
    It is now known that the connective constant (https://en.wikipedia.org/wiki/Connective_constant) of the honeycomb lattice is $\sqrt{2+\sqrt{2}}$, but if that were not rigorously known, would be the kind of thing you're looking for? – Sam Hopkins May 07 '19 at 19:40
  • 6
    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 07 '19 at 21:00
  • 1
    @Zidane, will you write that up as an answer? A version that also explains it without the words “rank”, “twist” and “L-function” would be especially welcome, and perphaps if you write the bare-bones answer, others can fill in the exposition. –  May 08 '19 at 01:36
  • @EGME, indeed, I was just providing the computation (up to a sign error) in a form that anyone can play with freely. –  May 08 '19 at 01:46
  • 13
    The article https://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 08 '19 at 06:47
  • @Zidane what Matt F. said. I believe that Stein did some explicit calculations with the curve of algebraic rank 4 and smallest conductor (he also calculated the analytic value of Sha to hundreds of decimal places IIRC, although that might have been for the rank 2 curve of smallest conductor). – Kevin Buzzard May 08 '19 at 08:38
  • 2
    @none that is the best answer I have yet seen! Please post as an answer! – Kevin Buzzard May 08 '19 at 08:41
  • 3
    @none: I think your example is both beautiful and closest to the spirit of the question. it would make a very nice answer. – Yaakov Baruch May 08 '19 at 08:42
  • @Zidane I guess it's hard (but not impossible) to make the ell curve example "explicit" -- the L-function doesn't converge for s=1 (even if written as the L-function of a grossencharacter -- one would have to turn the sum into an explicit integral which converges there, which should be possible by the techniques in Tate's thesis I guess, although "explicit" is now becoming less and less like a sensible adjective to use here...) – Kevin Buzzard May 08 '19 at 08:46
  • The Clausen function $\mathrm{Cl}_2(\theta)$ is just the Bloch-Wigner dilogarithm $D(e^{i\theta})$, which can be computed very efficiently e.g. in Pari/GP with polylog(2,exp(I*theta),2) – François Brunault May 08 '19 at 09:26
  • 3
    @none I believe this identity with $\pi^4$ is actually proven, Borwein in the article (see the reference in Wikipedia) says that "most but not all" identities of this type are proved, and this specific identity looks the simplest among them. – Fedor Petrov May 08 '19 at 10:30
  • 1
    @none : Mathematica (12) calculates none’s example exactly, so we can considered that proved! – EGME May 08 '19 at 11:28
  • Take $r$ to be a real number that is probably, but not provably, $0$. Then $\pi$ and $\pi+r$ fit your bill. – Asaf Karagila May 09 '19 at 06:32
  • 1
    @KevinBuzzard per Fedor Petrov and EGME, it looks like that formula has been proven, so it's not such a good answer after all. Oh well. It is sure cool! – none May 09 '19 at 09:06
  • I'm not sure you've defined "silly" in a useful way. For example, here's a case where we know how to compute the two numbers to gazillions of decimal places and yet it's still pretty silly: A = π, B = π with the n'th bit in its binary expansion flipped if Goldbach's conjecture fails at n. – Don Hatch May 09 '19 at 10:04
  • I don't know a rigorous definition of "silly", but on the other hand I am 100% convinced that this example falls under the "let's encode a well-known conjecture into a possibly slightly artificial real number" umbrella :D – Kevin Buzzard May 09 '19 at 13:58
  • 2
    How about the de Bruijn-Newman constant $\Lambda$? It's long been known that RH is true iff $\Lambda\le 0$. We now know that $0\le\Lambda\le 0.22$ which means RH is equivalent to $\Lambda=0$. So according to some, $\Lambda$ is probably 0, but it's obviously hard to prove. I wouldn't quite say this is silly in Kevin's sense. – none May 10 '19 at 05:28
  • 1
    I might be mistaken (I’m from CS, not a mathematician), but it seems to me that this has not much to do with the reals themselves, but rather to the language you use to express your identities. Your examples use transcendental functions and integration, but if you restrict the syntax to just polynomials, then equality is decidable on the reals (Tarski theorem) but not on integers (Hilbert’s tenth problem?). So are we talking about a specific set of operations? Is there an undecidability result regarding polynomials augmented with transcendental functions and/or integration? – Nicola Gigante May 26 '19 at 07:40
  • @gigabytes When people say "equality is undecidable for the reals" they are usually referring to computable real numbers. There are several equivalent formulations of them, but one is real numbers that have a (Turing) computable sequence of rational approximations. Perhaps you can see how if we could decide equality for these things we could solve the halting problem. – Robert Furber May 26 '19 at 22:21
  • I see, thanks for the clarification – Nicola Gigante May 27 '19 at 05:21

8 Answers8

45

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.)

Jason Rute
  • 6,247
  • 2
    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 08 '19 at 03:11
  • 10
    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 08 '19 at 08:31
  • Just to be clear -- the n on the left hand side of the equation in this answer is 7, right? – Kevin Buzzard May 08 '19 at 08:31
  • 1
    @KevinBuzzard Yes, $n=7$. I’ve made it explicit now. – Jason Rute May 08 '19 at 10:58
  • 2
    The "min" annoys me a bit in this example, for some reason I can't quite explain. – Kevin Buzzard May 11 '19 at 15:34
21

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}.$$

Timothy Chow
  • 78,129
  • 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 '19 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 '19 at 19:45
  • Oh this one would be perfect! Is it still open? – Kevin Buzzard May 12 '19 at 20:10
  • @KevinBuzzard : Jon Borwein told me about this ten years ago and it was open then. I believe it's still open; you could try emailing Jesus Guillera to check. You can find Guillera's email address on the arXiv, e.g., https://arxiv.org/abs/1807.07394 – Timothy Chow May 12 '19 at 20:22
  • 1
    @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 '19 at 16:41
  • @KevinBuzzard Moreover, he says there are many conjectured equalities like this which are open. Hopefully I will get a reference ... – EGME May 13 '19 at 16:51
  • @KevinBuzzard As per further inquiry, I can confirm that this cannot be handled by Mathematica at this time. However, maybe (I dare say likely) soon. – EGME May 13 '19 at 17:01
  • Many thanks for checking all this EGME! – Kevin Buzzard May 25 '19 at 22:15
  • Guillera's comment on this MO answer lists some other identities from his paper that were still unproven as of March 2018. – Timothy Chow Jul 29 '19 at 02:56
  • 2
    @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 '19 at 13:49
  • 1
    Gourevitch formula remains unproven. In principle, we can try to prove it by the WZ method (I have tried hard). The problem is that one needs to discover a suitable WZ pair, something which seems really very difficult and even could not exists. – Jesús Guillera May 30 '20 at 17:09
16

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).

Yaakov Baruch
  • 4,865
François Brunault
  • 20,484
16

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.

Yoav Kallus
  • 5,926
10

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$.

Robert Israel
  • 53,594
  • 20
    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 07 '19 at 19:21
9

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.

Kevin Buzzard
  • 40,559
3

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.

none
  • 31
  • It's not immediately clear (at least to me) why optimal sphere packing density is computable. I perhaps could agree for lattice packings (you can check for densities in fundamental regions of lattices), which is a special case known already to Gauss, but it's unclear how you would computably check for non-lattice packings. – Wojowu May 08 '19 at 08:29
  • 2
    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 08 '19 at 08:37
  • @KevinBuzzard As remarked above, Mathematica (12) calculates none’s example to the proposed answer ($17 \pi^4/360$), so we can consider that proved! – EGME May 08 '19 at 11:29
  • 3
    @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 08 '19 at 13:18
  • 3
    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: https://mathoverflow.net/questions/317692/is-there-a-short-proof-of-the-decidability-of-keplers-conjecture (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 08 '19 at 13:50
  • 1
    @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 09 '19 at 09:15
  • 4
    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 '19 at 01:52
  • 1
    @YoavKallus You are right. I was conflating computing the number and deciding if it was equal to $\pi/3\sqrt{2}$ (which is the point of the OPs question that these concepts are not the same). You algorithm is exactly right. Optimal packings in a cube where the balls can stick out are an over estimate and optimal packings where the balls don’t stick out is an under estimate. Hence we can compute the optimal packing in the limit to arbitrary accuracy. – Jason Rute May 11 '19 at 10:28
  • 1
    @YoavKallus, yes, thanks, that is a nice explanation. – none May 12 '19 at 03:11
2

In December of the year 2017 I discovered the following formula (but I could not prove it), see the addendum of this: $$ \sum_{n=1}^{\infty} \frac{(4n)!(2n)!(n!)^2}{(8n)!} \frac{120-1273n+2210n^2}{7^4(-2n+1)n^3} (-2401)^n \, {\overset{?}=} \, \sum_{n=1}^{\infty} \frac{\chi_{-7}(n)}{n^2}= L_{-7}(2), $$ a Dirichlet $L$ value (see here).

Jesús Guillera
  • 704