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?
 A: 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.
