In Fall 2024, I'm teaching CS 42: Principles and Practice of Computer Science, an intro course for students with significant prior programming experience.

I'm also Co-Director of the Math+CS Clinic Program with Prof. Talithia Williams (Math) and Prof. Ben Wiedermann (CS).

Definitely!

There has been remarkable progress on proof assistants like Coq, Isabelle, Agda, and Lean. Humans direct the high-level strategy (anywhere from breaking a goal into subgoals and applying simple logical steps, to invoking sophisticated proof-search tactics). The proof assistant fills in the details. The result is a proof with no ambiguities or omissions with every step justified; the computer can verify that the steps fit together correctly and that the proof is flawless.

In some parts of Computer Science, it's now typical for papers claiming a theoretical result to be accompanied by a computer-checked proof. Proof assistants have been making inroads into pure mathematics as well; a well-known example is the Flyspeck Project that used proof assistants to verify once and for all Thomas Hales's intricate proof of the Kepler Conjecture (i.e., that there is no denser packing of spheres than the familiar "pile of cannonballs" arrangement).

Often not. Proofs written for humans look like this:

Source

but popular proof assistants expect something much less readable, like:

Source

Source

One might worry that these proofs would be impossible to write, but proof assistant IDEs give huge amounts of guidance, and let the user focus on one small piece of the proof at a time. It's only when all the pieces are put together that it becomes impossible to see the forest for the trees.

It's fine to construct “write only” proofs when we only care that the final conclusion is true. If we just want to confirm our algorithm sorts all inputs correctly, or that our cryptographical protocol is secure, or that our programming language is type-safe, then any correct proof will do.

But in traditional mathematics, proofs are intended to be read and understood by humans; they give the reader broader insights into the topic by explaining why the result is true.

The disconnect is unfortunate. For example, the authors of the book Homotopy Type Theory verified all their claims using Coq before releasing the book in 2013. Yet to this day, the authors continue receiving reports of errors in the theorems and proofs in their book! The problem is that the theorems and proofs in the book were (re)written in the “traditional” fashion so readers could understand them. These English-language proofs were not formally verified, and typos and more serious errors slipped through.

A system that understands English-language proofs would be a great tool for students learning how to write proofs, and for researchers who want to check their proofs before publication. Computers already do spell-checking and grammar-checking, so why not logic-checking too?

There are proof assistants like Mizar, Isar, and Naproche whose input is more human readable, e.g.,

Source

Source

This is something I have been investigating recently, in collaboration with multiple undergraduate researchers. Being able to answer this question would tell us how close systems like Isar and Naproche are to handling input from arbitrary users.

We first downloaded over 1.6M papers from the popular arXiv.org preprint site, and found that 352K of these contained at least one proof. We then wrote a script to extract proofs from the LaTeX source code of these papers, resulting in 3.7M proofs (containing 558M words total). Because we were interested in the use of language, and not the technical results, we replaced all mathematical formulas by the placeholder MATH, resulting in sentences like Let MATH be the restriction of MATH to MATH.

We have spent most of our time buildling this language corpus, and have only scratched the surface of analyzing the language. A few preliminary observations:

• The sentence Without loss of generality we may assume that MATH. is twice as common as Without loss of generality we assume that MATH. and five times more common than We may assume without loss of generality that MATH.
• Mechanically extracted two-word collocations (words that appear together more often than can be explained by chance) include ad absurdum, almost surely, finitely many, pigeon hole, roughly speaking, and spherical harmonics. Longer collocations include induces an isomorphism between and it suffices to check that.
• Off-the-shelf NLP tools can do very badly on mathematical text. For example, when trying to identify the parts of speech for each word in the sentence Suppose MATH is even. the widely-used NLTK library identifies Suppose MATH as two proper nouns instead of a verb and a noun, and identifies even as an adverb instead of an adjective. But by retraining NLTK's part-of-speech tagger with a small collection of imperative sentences extracted from our data, we can get much better results.