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?
As a former mathematician who is now a programmer, it is I think inevitable that I have had similar dreams for a very long time; anyone with that common background would imagine broadly the same things. Like Dr. Wolfram, I have thought carefully not merely about the knowledge representation and UI issues in such a project, but also the difficulties in staffing and funding it. So it was with a feeling more of recognition than anything else that I received much of the essay.
To his great credit, Dr. Wolfram has done much – more than anyone else – to bring this vision towards reality. Mathematica and Wolfram Alpha are concrete steps towards it, and far from trivial ones. They show, I think, that the vision is possible and could be achieved with relatively modest funding – less than (say) the budget of a typical summer-blockbuster movie.
But there is one question that looms unanswered in Dr. Wolfram’s call to action. Let us suppose that we think we have all of the world’s mathematics formalized in a huge database of linked theorems and proof sequences, diligently being crawled by search agents and inference engines. In tribute to Wolfram Alpha, let us call this system “Omega”. How, and why, would we trust Omega?
There are at least three levels of possible error in such a system. One would be human error in entering mathematics into it (a true theorem is entered incorrectly). Another would be errors in human mathematics (a false theorem is entered correctly). A third would be errors in the search and inference engines used to trawl the database and generate new proofs to be added to it.
Errors of the first two kinds would eventually be discovered by using inference engines to consistency-check the entire database (unless the assertions in it separate into disconnected cliques, which seems unlikely). It was already clear to me thirty years ago when I first started thinking seriously about this problem that sanity-checking would have to be run as a continuing background process responding to every new mathematical assertion entered: I am sure this requirement has not escaped Dr. Wolfram.
The possible of errors of the third kind – bugs in the inference engine(s) – is more troubling. Such bugs could mask errors of the first two kinds, lead to the generation of incorrect mathematics, and corrupt the database. So we have a difficult verification problem here; we can trust the database (eventually) if we trust the inference engines, but how do we know we can trust the inference engines?
Mathematical thinking cannot solve this problem, because the most likely kind of bug is not a bad inference algorithm but an incorrect implementation of a good one. Notice what has happened here, though; the verification problem for Omega no longer lives in the rarefied realm of pure mathematics but the more concrete province of software engineering.
As such, there are things that experience can teach us. We don’t know how to do perfect software engineering, but we do know what the best practices are. And this is the point at Dr. Wolfram’s proposal to build Omega on Mathematica and Wolfram Alpha begins to be troubling. These are amazing tools, but they’re closed source. They cannot be meaningfully audited for correctness by anyone outside Wolfram Research. Experience teaches us that this is a danger sign, a fragile single point of failure, and simply not tolerable in any project with the ambitions of Omega.
I think Dr. Wolfram is far too intelligent not to understand this, which makes his failure to address the issue the more troubling. For Omega 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.
I would go so far as to say that any mathematician or software engineer asked to participate in this project is ethically required to insist on complete auditability and open source. Otherwise, what has the tradition of peer review and process transparency in science taught us?
I hope that Dr. Wolfram will address this issue in a future blog post. And I hope he understands that, for all his brilliance and impressive accomplishments, “Trust my secret code” will not – and cannot – be an answer that satisfies.