There is a striking similarity between writing a computer program and proving a theorem. A computer program is a sequence of fine-grained instructions for realizing some desired computation. A proof is a sequence of fine-grained deductive steps for justifying some desired claim. The Proofs-as-Programs paradigm in computer science (CS) formalizes this analogy: Logical propositions are nothing more than data types, of the same ilk as, say, floating point numbers and binary trees of integers; and proofs are nothing more than computer programs, whose output are data of the desired data types.
Applications of CS to Math
While long understood since at least the 1960s, internal developments within the theory of (abstract data) types have made the Proofs-as-Programs paradigm a natural formalization of mathematics as it is actually taught and practiced. Paige North observes:
The specification of standard dependent type theory is much closer to how we use it than is the specification of ZF set theory. For example, functions are defined by two rules: (1) You can create a function by giving a formula, and (2) you can use a function by applying it to an element of its domain. This is usually how we teach students to use functions anyway. So, when we teach students the fundamentals of math using type theory, there’s no complicated set theory that’s getting swept under the rug — everything is accessible to them, and I think this is a better position from which to teach.
As such, the paradigm has attracted renewed pedagogical and research interest in math and CS departments around the world. The most prominent example is the Xena Project [1], headed by Kevin Buzzard at Imperial College in London: a project to formalize and teach the entire undergraduate mathematics curriculum — both the statements and proofs of all major theorems — in Lean, a programming language designed for theorem-proving. At Ohio State, Jim Fowler and Paige North have been recently introducing undergraduates to the paradigm.
A screenshot of Lean code that Paige used with some students.
Paige North had been teaching type theory to high school students last summer in the Ross Mathematics Program. The subject matter was well adapted for an online format, to which, incidentally the Ross Program this coming summer must adapt. All her students submitted their assignments in a cloud-based mathematics notebook, which can compile, or equivalently evaluate the correctness of, all proofs. Instead of explicitly teaching the Proofs-as-Programs paradigm, Paige implicitly conveyed its essence through the exercises.
The most important message I wanted to convey by using Lean is that proofs *are* themselves mathematical objects. With enough practice, you can (often) write a proof just like you would compute an integral: There are some steps you must always take and some tricks to learn that you can sometimes apply. I think sometimes what constitutes a correct proof can seem like a social construct (indeed it is when we leave out most of the details), and it’s helpful to start students off with something more tangible.
Interestingly, type theory provided an alternative pedagogical route to advanced mathematics; Paige notes:
Dependent type theory brought together a lot of the wisdom earned by the logicians, theoretical computer scientists and category theorists of the midcentury, and later by the homotopy theorists and higher category theorists when Voevodsky proposed the Univalence Axiom. When I taught the Ross course, since I did not want to assume any knowledge of other mathematics, I stuck to teaching just type theory (instead of exploring interesting connections with other subjects). It was interesting to see how quickly (weeks instead of years) and easily you can get to the type-theoretic version of many points of “advanced” mathematics — from homotopy theory, topos theory and higher category theory. I didn’t quite appreciate this before teaching the Ross course because I always considered type theory within the larger context of these other subjects.
Jim Fowler had been supervising a group of undergraduates in learning the Lean-alternative Agda and its mathematical foundations [3] this past semester, with the goal of creating an undergraduate research project out of the studies. For Jim, this kind of computerization of mathematics keeps traditional subjects relevant in the digital age:
I think provably correct computer systems are also very much in our future, and as much as I think math departments should absolutely be pushing toward data science, we should also be preparing the more algebraically minded of our (under)graduate students to know how to use computers to prove things.
Homotopy Type Theory (HoTT): One of the most striking internal developments in type theory is the nascent subfield of Homotopy Type Theory (HoTT). HoTT is an interpretation of data types as spaces, and a certain higher order logic of data types as their homotopy theory. Paige headed up a graduate reading seminar on HoTT last year and has helped make Ohio State one of the founding members of the Midwest HoTT Workshops. Niles Johnson notes:
Formally verified proofs in homotopy theory would be unthinkable without the perspective of homotopy type theory. By building homotopy-theoretic concepts into the foundations of the subject, nontrivial calculations become approachable (I'm thinking here of the calculations of low-dimensional homotopy groups of spheres). Implementing theoretical tools such as Whitehead products or Toda brackets is definitely within reach.
Applications of Math to CS
HoTT opens up automated theorem-proving to methods from topology. Governmental funding interest in HoTT stems in part from its potential to provide new tools in the seemingly intractable problem of proving the safety of complex, engineered systems. For example, Paige’s research is partially supported by an Air Force Office of Research grant on cybersecurity. These kinds of applications can help ensure the relevance of research-level mathematics. Jim observes:
It's refreshing to think that there are maybe 4 million software engineers in the U.S., and maybe 20 thousand "research mathematicians", but imagine if we could convince just 1% of software engineers that they needed to be "proofgrammers" as well as programmers.
Article contributed by Sanjeevi Krishnan
References
[1] An introduction to the Xena Project: https://xenaproject.wordpress.com/what-is-the-xena-project/
[2] An online Lean tutorial that Paige uses with her undergraduates: https://leanprover.github.io/documentation/
[3] An online Agda tutorial that Jim uses with his undergraduates: https://plfa.github.io/
