Hcfyk

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^thetalog|2sin(sigma)|dsigma$$

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

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

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

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}} + 5sqrt{frac{2}{5 + sqrt{5}}} + 5sqrt{frac{1 + sqrt{5}}{2sqrt{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.)

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