Proof, in the form of step by step deduction, following the rules of logical reasoning, is the ultimate test of validity in mathematics. Some proofs, however, are so long or complex, or both, that they cannot be checked for errors by human experts. In response, a small but growing community of mathematicians, collaborating with computer scientists, have designed systems that allow proofs to be verified by machine. The success in certifying proofs of some prestigious theorems has led some mathematicians to propose a complete rethinking of the profession, requiring future proofs to be written in computer readable code. A few mathematicians have gone so far as to predict that artificial intelligence will replace humans in mathematical research, as in so many other activities.
One's position on the possible future mechanization of proof is a function of one's view of mathematics itself. Is it a means to an end that can be achieved as well, or better, by a competent machine as by a human being? If so, what is that end, and why are machines seen as more reliable than humans? Or is mathematics rather an end in itself, a human practice that is pursued for its intrinsic value? If so, what could that value be, and can it ever be shared with machines?
All Helix Center events are free and open to the public, including this one!
Roundtables are streamed live our website and the recording remains available after the event events.
This is a past event that happened on Saturday, October 5th, 2019 at 2:30pm.
Participants
Stephanie Dick
Assistant Professor, History and Sociology of Science, University of Pennsylvania
Stephanie Dick is an Assistant Professor of History and Sociology of Science at the University of Pennsylvania. She received her PhD in History of Science from Harvard University in 2015 and was a Junior Fellow at the Harvard Society of Fellows prior to joining the faculty at Penn. Her work sits at the intersection of... read more! »
Branden Fitelson
Distinguished Professor of Philosophy, Northeastern University
Branden Fitelson is Distinguished Professor of Philosophy at Northeastern University. Before teaching at Northeastern, Branden held teaching positions at Rutgers, UC-Berkeley, San José State, and Stanford and visiting positions at the Munich Center for Mathematical Philosophy at LMU-Munich (MCMP @ LMU) and the Institute for Logic, Language and Computation at the University of Amsterdam (ILLC... read more! »
Thomas Callister Hales
Mellon Professor of Mathematics, University of Pittsburgh
Thomas C. Hales is the Mellon Professor of Mathematics at the University of Pittsburgh. He received B.S. and M.S. degrees from Stanford University, a Tripos Part III from Cambridge University, and a Ph.D. from Princeton University in representation theory under R. P. Langlands. He has held postdoctoral and faculty appointments at MSRI, Harvard University, the... read more! »
Michael Harris
Professor of Mathematics, Columbia University
Michael Harris is Professor of Mathematics at Columbia University; before that he held positions at Brandeis University and Université Paris-Diderot. He obtained his Ph.D. in 1977 from Harvard University, under the direction of Barry Mazur. He has organized or co-organized more than 20 conferences, workshops, and special programs in his field of number theory. He... read more! »
Francesca Rossi
IBM Fellow & IBM AI Ethics Global Leader
Francesca Rossi is an IBM Fellow and the IBM AI Ethics Global Leader. She is based at the T.J. Watson IBM Research Lab, New York, USA, where she leads AI research projects. She co-chairs the IBM AI Ethics board and she participates in many global multi-stakeholder initiatives on AI ethics, such as the Partnership on... read more! »
It’s about time
Really interesting.
Related in the news Sep 26 2019:
Number Theorist Fears All Published Math Is Wrong
https://www.vice.com/en_us/article/8xwm54/number-theorist-fears-all-published-math-is-wrong-actually
“I think there is a non-zero chance that some of our great castles are built on sand,”
he said, arguing that we must begin to rely on AI to verify proofs.
The “all published maths is wrong” quote (attributed to me) is taken out of context really — I was talking about the discussion Michael, Patrick Massot and I led in Paris at the intersem. https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ are some comments which perhaps clarify what my real beliefs are, without having them run through a journalist.
(This was initially going to be a comment on Michael Harris’ blog but it got too long)
Excellent discussion. But I disagree with the frame that these conversations always take.
If you are going to frame the role of computers in math as the “mechanization of mathematics” it’s no wonder that a major theme of the discussion will be the threat computers pose to the humanism of math. It presupposes the form that computers can contribute to mathematics, but honestly, this is far from a given.
The reason we frame the role of computers this way is to some extent circular. It’s inspired by existing technologies and research programs but those in turn define what we regard as the role of computers in math. The frame is also a function of our biases and what we personally have at stake. It seems that a big motivating factor is proof verification because there are instances where nobody else can check a proof, the experts die off, or some other reason. Also most mathematicians working on this project seem supremely adept at abstract math and are able to much more fully appreciate the beauty of arithmetic geometry for instance. They are closer to Lefschetz as you describe him [on Harris’ blog is a quote “Lefschetz never stated a false theorem nor gave a correct proof.”] . They already have mathematical intuition, so it is something to be lost, whereas for most other people computers only have the possibility of making those subjects intelligible.
Given these biases we are much less likely to recognize the work of someone like Bret Victor as having transformative potential for research math. I would however recommend Michael Nielsen’s essays which disseminate some of Victor’s ideas in a more palatable form. See for instance “Reinventing Explanation”.
Another reason that we have the frame we have now is that all the people working outside of it had no ambition for using their work to meet the challenges of abstract math. Consequently people doing serious math could easily ignore their work. For instance Seymour Papert in Mindstorms talked about creating a “mathland” (with the logo turtle) that children could inhabit to learn math just as children in France learn french. The idea that such a mathland could be used to teach children honest differential geometry is naive but the spirit is profound. We create “mathlands” of sorts with our formal theories and we “play” in them all the time, but some of us are more adept to these kinds of environments than others. We never ask how computers can be used to really enrich these environments.
To give a concrete example, think about a person learning spectral sequences for the first time. They consult a number of resources, including Hatcher, Bott and Tu, Chow, and Mosher and Tangora. These resources have a variety of approaches and notation. At the same time they each have complimentary perspectives that one would want to integrate into a coherent and complete picture. Let’s focus further on the spectral sequence of a filtered complex, comparing the expositions of Chow’s article and Mosher and Tangora’s book. The schtick of Chow’s article is an intuitive development of the concept of the spectral sequence of a filtered complex, “you could have invented spectral sequences”, taking the reader step by step to closer approximations of the associated graded complex associated to the filtration of the actual homology we are interested in. Mosher and Tangora by contrast begin with the the construction of exact couples. They then apply it to an exact couple derived from a filtered complex. They show that it converges under some circumstances. Ideally one would like to “line up” the two developments, realizing exact couples as the seat of the pants method in Chow. What kind of computer enabled tools could help with this “lining up”? Certainly nothing resembling “mechanizing” (unless you want to solve Hilbert’s 24th problem while you’re at it).
Here is a much more modest example. In any subject there is a “primordial soup” of foundations and different ways to go about developing the subject. In linear algebra you can nearly enumerate all of these but it always escapes intelligibility. Is a matrix a set of row vectors stacked on top of each other, or is it a set of column vectors side by side, or is it just an m by n array? Are row vectors and column vectors primitives or are they just 1 by n or m by 1 matrices? On which definition of a matrix is matrix multiplication defined? How can we interpret matrix multiplication with those different definitions? How are they equivalent? How do the higher level abstractions parameterize lower level interpretations? For example when you start talking about abstract vector spaces and linear maps you can think of column vectors as linear maps from the field to the vector space. You can then think of a linear map evaluated on a vector as a composition of linear maps corresponding to the multiplication of matrices. From this depending on your interpretation of (compositions of) linear maps you can recover the matrix/row/column-vector interpretations. I can almost spell this out, but not quite.
I find it extremely hard to put in words what I want to describe, because in the words of George Orwell, “the existing dialect will come rushing in and do the job for you, at the expense of blurring or even changing your meaning”. Whatever I can put in sufficiently clear terms gets flattened to the existing dialect (abstraction, axioms, linear logical development) while that is just what I want to break away from. Consequently, I can only point towards some tension, which I hope you and others can see.
Here is a poor metaphor. Each logical development is like finding a maximal subtree of a graph. This graph is embedded in a space with various axes of abstraction. Understanding the subject matter is a matter of being able to quickly navigate this space. Bourbaki in “The Architecture of Mathematics” talks about abstraction and the axiomatic method as a way of restoring the intelligibility of the subjects, but when the problem is navigating details or moving up and down the latter of abstraction, this is inadequate for all but a few. Case in point is an eclectic subject like algebraic topology.
This suggests that the entire architecture of math (a la Bourbaki), with theorems deduced in a linear fashion using the axiomatic method, should be rethought. The reason we cannot break away from this type of architecture I claim is not intrinsic to math but intrinsic to the media we do math in. With computer enabled “dynamic” media I can conceive of an architecture of mathematics that admits nonlinear logical development, that preserves the power of math and greatly extends its accessibility.
In less grandiose terms it seems that there are some structures we can reasonably abstract and there are some other structures that we cannot reasonably abstract. You can’t abstract them because the real problem is navigating the details while abstraction is about hiding the details. We have the infrastructure to establish the truth of claims but we don’t have that infrastructure for exploring why those claims are true. I suppose I believe math would be a lot more ‘democratic’ if there was such infrastructure and it took less extraordinary minds to fill in the understanding-gaps given their obvious implications for filling in the logical-gaps.
Anyway, thats my take on the potential for computers in math. Even if you don’t agree I’d hope you and others take a more aggressive stance trying to understand how to use computers to actively extend the humanity of mathematics and not just try to preserve it.