A Closed Future for Mathematics? by Eric Raymond.
From the post:
In a blog post on Computational Knowledge and the Future of Pure Mathematics Stephen Wolfram lays out a vision that is in many ways exciting and challenging. What if all of mathematics could be expressed in a common formal notation, stored in computers so it is searchable and amenable to computer-assisted discovery and proof of new theorems?
…
… to be trusted, the entire system will need to be transparent top to bottom. The design, the data representations, and the implementation code for its software must all be freely auditable by third-party mathematical topic experts and mathematically literate software engineers.
Eric identifies three (3) types of errors that may exist inside the proposed closed system from Wolfram.
Is transparency of a Wolfram solution the only way to trust a Wolfram solution?
For any operation or series of operations performed with Wolfram software, you could perform the same operation in one or more open or closed source systems and see if the results agree. The more often they agree for some set of operations the greater your confidence in those operations with Wolfram software.
That doesn’t mean that the next operation or a change in the order of operations is going to produce a trustworthy result. Just that for some specified set of operations in a particular order with specified data that you obtained the same result from multiple software solutions.
It could be that all the software solutions implement the same incorrect algorithm, the same valid algorithm incorrectly, or errors in search engines searching a mathematical database (which could only be evaluated against the data being searched).
Where N is the number of non-Wolfram software packages you are using to check the Wolfram-based solution and W represents the amount of work to obtain a solution, the total work required is N x W.
In addition to not resulting in the trust Eric is describing, it is an increase in your workload.
I first saw this in a tweet by Michael Nielsen.