# How can we be sure that results that rely heavily on extensive computations are correct?

Recently a ''bug'' was discovered in one of the most popular mathematics software, Wolfram Mathematica (see links here and here). It concerns the evaluation of the sum $$\sum_{k=1}^{n-1} \frac{(-1)^{k-1}(k-1)!^2}{(n^2-1^2)\ldots(n^2-k^2)},$$ a fairly straightforward computational exercise, as one would expect. Surprisingly, Mathematica incorrectly evaluates this sum to $$\frac{1}{n^2},$$ instead of the correct expression, which is $$\frac{1}{n^2}-\frac{2(-1)^{n-1}}{n^2 \binom{2n}{n}}.$$

Another user (in second link above) found that Maple 2020 also makes the same incorrect evaluation.

This raises the question whether we can trust widely used software like Mathematica and Maple with (much) more complex computational tasks, and in particular theorems and lemmas that appear in published literature that explicitly rely on large scale computations performed with such applications.

In some cases, the peer review process involves replicating computational results that appear in a manuscript, but this is (more often than not) not the case. Furthermore, it is not unlikely that reviewers will use the same software to double check these results as the author, thereby replicating the same mistake, or bug.

To what extent can we trust results that were obtained with the aid of extensive computations? At what point can we safely accept the ''truthfulness'' of a claim if its replication requires months (sometimes years) of number crunching performed by software that can make such elementary mistakes as above?

• One countermeasure is using Maple and Mathematica and Sagemath and ... I hink that this problem is very deep and can only be resolved for simple problems with algorithms that are provable correct (may be that this depends on the concrete implementation, the processor used, ...) The same problem is with problems which are solved without such programs. How can we trust that we don't make a hidden mistake? – Dieter Kadelka Dec 11 '20 at 12:41
• The answer is that we can't in general trust such calculations but we can check them. Repeating the calculation the same way, even using a different package, is not a great check as this example shows. A sum like this should be checked numerically, which would have caught the error immediately. On other occasions, there are different ways to arrange the calculation, or non-trivial sanity checks that can be done. – Brendan McKay Dec 11 '20 at 13:02
• This is a really interesting/disturbing bug you found! – Sam Hopkins Dec 11 '20 at 20:20
• – Timothy Chow Dec 11 '20 at 23:32
• The heavily computational parts of my papers are the parts that are least likely to contain errors. The odds of hitting an error like this one and not noticing it numerically is much much lower than the odds of my screwing up a proof. – Noah Snyder Dec 12 '20 at 15:44

In the long run, the best we can probably do is to develop computer algebra packages whose computations are formally verified. To my knowledge, there has not been a lot of effort in this direction. Muhammad Taimoor Khan’s 2014 Ph.D. thesis, Formal Specification and Verification of Computer Algebra Software, provided a proof of concept; he implemented a fragment of Maple that he called MiniMaple and formally verified a particular package of routines for Gröbner basis computations.

At the present time, however, there seems to be little demand for computer algebra systems that meet the bar of formal correctness, in part because the sacrifice in computational speed for the sake of increased certainty does not appeal to most people. Thus, people who want their computations to be formally correct have to code them up on an ad hoc basis. For example, the original Hales–Ferguson proof of the Kepler conjecture involved heavy computations that were carried out using traditional software packages such as CPLEX. When it came to producing a formally verified version of these computations for the Flyspeck proof, there was no royal road; the computations had to be completely re-programmed from scratch. I am not sure exactly what the slowdown factor was when passing from the traditional computation to the formally verified computation, but as reported in A formal proof of the Kepler conjecture, the formally verified versions of the computations took more than 5000 processor-hours to complete. Moreover, even Flyspeck has some potential loopholes; see Mark Adams's presentation on Flyspecking Flyspeck for an interesting discussion.