Using Computer to Verify Math Theorems

Source: Quanta, May 2015

For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people.

“The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes,” Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error.

The accepted foundation of mathematics is set theory. Like any foundational system, set theory provides a collection of basic concepts and rules, which can be used to construct the rest of mathematics. Set theory has sufficed as a foundation for more than a century, but it can’t readily be translated into a form that computers can use to check proofs. So with his decision to start formalizing mathematics on the computer, Voevodsky set in motion a process of discovery that ultimately led to something far more ambitious: a recasting of the underpinnings of mathematics.

Set theory as a foundation includes these basic objects — sets — and logical rules for manipulating those sets, from which the theorems in mathematics are derived. An advantage of set theory as a foundational system is that it is very economical — every object mathematicians could possibly want to use is ultimately built from the null set.

On the other hand, it can be tedious to encode complicated mathematical objects as elaborate hierarchies of sets. This limitation becomes problematic when mathematicians want to think about objects that are equivalent or isomorphic in some sense, if not necessarily equal in all respects.

In place of set theory, Russell’s system used more carefully defined objects called types. Russell’s type theory begins with a universe of objects, just like set theory, and those objects can be collected in a “type” called a SET. Within type theory, the type SET is defined so that it is only allowed to collect objects that aren’t collections of other things. If a collection does contain other collections, it is no longer allowed to be a SET, but is instead something that can be thought of as a MEGASET — a new kind of type defined specifically as a collection of objects which themselves are collections of objects.

From here, the whole system arises in an orderly fashion. One can imagine, say, a type called a SUPERMEGASET that collects only objects that are MEGASETS. Within this rigid framework, it becomes illegal, so to speak, to even ask the paradox-inducing question, “Does the set of all sets that do not contain themselves contain itself?” In type theory, SETS only contain objects that are not collections of other objects.

An important distinction between set theory and type theory lies in the way theorems are treated. In set theory, a theorem is not itself a set — it’s a statement about sets. By contrast, in some versions of type theory, theorems and SETS are on equal footing. They are “types” — a new kind of mathematical object. A theorem is the type whose elements are all the different ways the theorem can be proved. So, for example, there is a single type that collects all the proofs to the Pythagorean theorem.

Spaces are homotopy equivalent if, roughly speaking, one can be deformed into the other by shrinking or thickening regions, without tearing.

Infinity-groupoids encode all the paths in a space, including paths of paths, and paths of paths of paths. They crop up in other frontiers of mathematical research as ways of encoding similar higher-order relationships, …

Voevodsky was able to create an interpretation of type theory in the language of infinity-groupoids, an advance that allows mathematicians to reason efficiently about infinity-groupoids without ever having to think of them in terms of sets. This advance ultimately led to the development of univalent foundations.

To him <VV>, the real potential of type theory informed by homotopy theory is as a new foundation for mathematics that’s uniquely well-suited both to computerized verification and to studying higher-order relationships.

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.”

Following the special research year, activity split in a few different directions. One group of researchers, which includes Shulman and is referred to as the HoTT community (for homotopy type theory), set off to explore the possibilities for new discoveries within the framework they’d developed.

Another group, which identifies as UniMath and includes Voevodsky, began rewriting mathematics in the language of univalent foundations. Their goal is to create a library of basic mathematical elements — lemmas, proofs, propositions — that mathematicians can use to formalize their own work in univalent foundations.

Related Resource: Quanta, Feb 2013

… proofs, where computers are playing an increasingly prominent role, are not always the end goal of mathematics. “Many mathematicians think they are building theories with the ultimate goal of understanding the mathematical universe,” said Minhyong Kim, a professor of mathematics at Oxford University and Pohang University of Science and Technology in South Korea.

Mathematicians try to come up with conceptual frameworks that define new objects and state new conjectures as well as proving old ones. Even when a new theory yields an important proof, many mathematicians “feel it’s actually the theory that is more intriguing than the proof itself,” Kim said.