An article in a recent issue of New Scientist highlights the potential partnership between computers and mathematicians. It begins with an account of the use of computers in a proof that would do little, it seems, to provide greater understanding, or greater insight into the content of the idea the proof explores. The computer program merely exhausts the counter examples of a theorem, thereby proving it true (a task far too impractical to attack by hand). Reviewing this kind of proof, however, requires checking computer code, and this is something that referees in mathematics are not likely to want to do. And so efforts have been made to make the checking easier by employing something called a ‘proof assistant.’ The article doesn’t do much to clarify how the ‘proof assistant’ works, and says just a little about how it makes things easier. But a question that comes to mind quickly for me is whether such a proof could reveal new bridges between different sub-disciplines of mathematics, the way the traditional effort has been known to do.
A discussion of the work of prominent mathematician Vladimir Voevodsky follows. This work takes us back to foundational questions and clearly addresses those bridges. While mathematics is grounded in set theory, set theory can permit more than one definition of the same mathematical object. Voevodsky decided to address the problem that this creates for computer generated proofs.
…if two computer proofs use different definitions for the same thing, they will be incompatible. “We cannot compare the results, because at the core they are based on two different things,” says Voevodsky.
Voevodsky swaps sets for types described as “a stricter way of defining mathematical objects in which every concept has exactly one definition.
“This lets mathematicians formulate their ideas with a proof assistant directly, rather than having to translate them later. In 2013 Voefodsky and colleagues published a book explaining the principles behind the new foundations. In a reversal of the norm, they wrote the book with a proof assistant and then “unformalized” it to produce something more human-friendly.
There’s a very well-written description of the history and recent successes of Voevodsky’s work in a Quanta Magazine piece from May 2015. Voevodsky’s new formalism is called the univalent foundation of mathematics. The Quanta article describes how these ideas grew from existing formalisms in reasonable detail. But, what I find most interesting is the surprising consistency among particular ideas from computer science, logic and mathematics.
This consistency and convenience reflects something deeper about the program, said Daniel Grayson, an emeritus professor of mathematics at the University of Illinois at Urbana-Champaign. The strength of univalent foundations lies in the fact that it taps into a previously hidden structure in mathematics.
“What’s appealing and different about [univalent foundations], especially if you start viewing [it] as replacing set theory,” he said, “is that it appears that ideas from topology come into the very foundation of mathematics.”
One of the youngest sub-disciplines finds its way into the foundation, a very appealing and suggestive idea. Finding hidden structure is what always looks magical about mathematics. And it is, fundamentally, what human cognition is all about.
There’s a nice report on one of Voevodsky’s talks in a Scientific American Guest Blog from 2013 by Julie Rehmeyer that includes a video of the talk itself.
This topic requires a closer look, which I expect to do with a follow-up to this post.
Recent Comments