Reading a book by Jaron Lanier is a reminder that (some?) Silicon Valley engineers are calmly planning to turn each of our deepest science fiction nightmares into the Next Big Thing. We have seen that Amir Alexander speculates that the “computer nerd” or “wiz” could be the next face of mathematics in the popular imagination; but what if the imagined mathematician of the future is an artificial intelligence, a distributed network with no face at all?
Here is Henri Poincaré in his 1908 text Science and Method, defending his conception of mathematics against logicism in the mode of Bertrand Russell:
There is a reality more subtile, which makes the very life of the mathematical beings, and which is quite other than logic.… When the logician shall have broken up each demonstration into a multitude of elementary operations, all correct, he still will not possess the whole reality; this I know not what [je ne sais quoi] which makes the unity of the demonstration will completely escape him.
Even with the help of the elephant that makes a brief appearance (!) between these two sentences, this is a fragile defense of the human perspective in mathematics. The je ne sais quoi is not obviously a notion that lends itself to precise formalization, and I really don’t see how an automated proof assistant will recognize it , nor how an automated theorem prover will mobilize it to define directions of research that a human partner will endorse as indispensable.
(Someone should study the apparently superfluous but recurring references to elephants in philosophical reflections on mathematics. There is one in Chapter 7 of Mathematics without Apologies; I really can’t explain how it got there.)
Poincaré was not specifically disagreeing with David Hilbert’s claim in his 1900 Paris address:
“In mathematics there is no ignorabimus” [we will not know] nor was Hilbert specifically responding to Poincaré thirty years later when he proclaimed in Königsberg his celebrated slogan: “Wir müssen wissen — wir werden wissen!” (‘We must know — we will know!’). If Poincaré is the romantic of this post then Hilbert is the proto-nerd; but neither of these two titans really fits Alexander’s narrative frame.
A friend from the Computer Science department at Boston University is in town today. When he was a graduate student, the founders of AI were convinced that by the year 2000 we wouldn’t have to prove theorems any more; we would just feed the axioms into the system and theorems would pop out. This was supposed to be good news, an idea that makes as much sense to me as the expectation that humans would celebrate if babies could be bred in bell jars, because we wouldn’t have to bother with sex any more.
My friend doesn’t think computers will ever replace mathematicians, but he has been working with automated proof assistants. He describes their output as “boring.” The normal proof that the square root of 2 is irrational takes up 10 lines, but a proof assistant’s proof fills 15 pages. (Mathematics without Apologies proves this in two pages, but a lot of that is motivation and background.) A proof assistant can’t say “this step is obvious.” An artificial mind lacks the notion of obviousness. When you have some familiarity with the computer’s proof, my friend informed me, you can read it just as you would a normal proof. Like learning a new language.
My article Do Androids Prove Theorems in Their Sleep? was mainly about how we might communicate with artificial theorem provers. Will they spontaneously meet us halfway? Or will it be up to us to adjust (if the computers bother communicating with us at all)? Jaron Lanier writes:
A book isn’t an artifact, but a synthesis of fully realized individual personhood with human continuity.
I would like to say that a theorem isn’t an artifact either. Lanier goes on:
Thinking about people as components on a network is—in intellectual and spiritual terms—a slow suicide for the researchers and slow homicide for everyone else.
Applied to the question at hand, this means that by erecting the wrong protections to defend the fortress of mathematical certainty from the “subtilety” of Poincaré’s je ne sais quoi, we will end up starving ourselves into submission.
P.S. I should have checked: “Dawn of the Nerds” is already the name of an online gaming community. It seems to have absolutely nothing to do with the two posts of that name on this blog (and the two future posts to which I have committed myself). My apologies if you came here for gaming.