Mathematics and Formality

Table of Contents

My Journey in Learning Mathematics

When I was deciding whether to pursue a Ph.D., one of the most enticing reasons was the opportunity to strengthen my math skills. I’ve always loved math, but I feel I’m lacking in some areas. I’ve only taken courses in calculus and discrete math, and I want to learn more.

In my first semester at Brown, I took Frontiers of Graph Algorithms, and in my second semester, I took Algorithmic Game Theory. Both courses are math-heavy but offer fantastic content that shows how to apply mathematical knowledge in computer science. I’ve also started reading Proofs: A Long-Form Mathematics and Real Analysis: A Long-Form Mathematics. These books provide foundational concepts in math that are useful for my research in artificial intelligence.

Reflections on Theorem Proving

A surprising sentiment I had during the courses and while solving problems in both books is that proving theorems is not as formal as I expected. Let me elaborate: the arguments aim to convince the reader of the proof’s correctness but can skip details or computations of certain equations. This feels a bit off to me as a computer scientist—if I skip a step in an algorithm or miss a semicolon, my program won’t compile or will generate incorrect results. This feels much stricter than proving theorems, and I’ve always believed there is nothing more rigorous in science than math.

Interestingly, I found that I’m not the only one who feels this way. I came across the following quote in a research paper:

The standard of correctness and completeness necessary to get a computer program to work at all is a couple of orders of magnitude higher than the mathematical community’s standard of valid proofs.

• William P. Thurston

I’ve been exploring the use of proof assistants, which allow me to write completely formal proofs. It’s cool to use my coding skills for math-related thinking, and I really enjoy it.

Why Formality Matters?

I find formality especially important when learning math. First, I don’t always have a professor to review my arguments, so using a proof assistant to validate my proofs ensures I’m not misleading myself. Additionally, since I’m learning, having this feedback loop where I see the proof compile helps me move faster into new concepts. Another key point is that since I’m learning, getting quick feedback when I see the proof compile allows me to move faster onto new concepts.

Using proof assistants has also gained traction in the mathematical community. Terence Tao made a blog post explaining how he formalized a theorem from one of his papers. The Liquid Tensor Experiment is a great example of why formalizing mathematical arguments is exciting, even beyond my goal of learning math. Formalizing proofs is the difference between 99% certainty and absolute certainty, and for important theorems, that 1% makes a big difference.

I hope I’ve convinced you that formal proofs are cool and especially useful when learning math.

So, What’s the Plan?

I’ll try to learn Lean 4. Why? Well, no other reason than the fact that Terence Tao uses it. I know there’s an authority bias, but what do you expect me to do? Go against Terence? No way!

You might expect me to dive right into formalizing proofs for my classes or the exercises in the books I’m reading. As much as I’d love to be smart enough to accomplish that, it seems that without any prior simpler work, I wouldn’t be able to do it.

My plan is to start by formalizing some concepts in propositional logic. Why? In my opinion, propositional logic fits well into the formal proof framework. Since I’ve taken logic and discrete math as an undergrad, I’m comfortable with the concepts, allowing me to focus on learning Lean. I’ll use the ForallX book by P.D. Magnus et al. I’ve been looking for an excuse to read it, and this seems like the perfect opportunity.

I’ll be adding the proofs for each exercise from the book in this GitHub repo. Since not all exercises are suitable for formalization, I’ll only include the ones that can be. My goal is to complete a chapter per day, starting from Chapter 17, where formal proofs begin to appear.

Building a Lean Proofs

A Lean proof can be either a Theorem or an Example. Theorems allow you to name the proof, so you can use them later in other proofs. In contrast, Examples are nameless and can’t be referenced later in the code.

Here’s an example of a Lean proof. I’m trying to show that with $M \lor (N \rightarrow M)$ as a premise, it’s possible to arrive at $\lnot M \rightarrow \lnot N$ as a conclusion. The proof includes the types of each proposition, a set of premises, and the conclusion you need to reach.

example {M N: Prop} (p₁: M ∨ (N → M)) : ¬M → ¬N := by
  intro h₁
  cases p₁ with
  | inr h₂ =>
    have s₁: ¬N := modus_tollens ⟨h₂, h₁⟩
    exact s₁
  | inl h₂ => contradiction

In this proof, since we are proving $\lnot M \rightarrow \lnot N$, we start by assuming $\lnot M$ and setting $\lnot N$ as the new goal because we’re proving an implication. Now, with a premise that has an “or” connector, we can handle the disjunction by considering two cases: one where the left side is true and the other where the right side is true. We then use modus tollens in the first case and apply the explosion rule in the second case to reach the conclusion from the contradiction.

Cheat Sheet

Here are some examples of how to deal with different types of goal propositions:

• When your goal is $p \leftrightarrow q$, use constructor to create sub-goals of $p \rightarrow q$ and $q \rightarrow p$.
• When your goal is $p \rightarrow q$, use intro to assume $p$ and get $q$ as the new goal.
• If you have $p \lor q$, use left or right to focus on either $p$ or $q$ in the goal.
• If you have $p \land q$, use constructor to break it into sub-goals $p$ and $q$.

In the repo, I’ve added the deduction rules needed to solve the exercises in the book. You can use them by adding import ForallX.rules at the top of your file. Here are some examples of the rules:

• When you have $P \lor Q$ and $\lnot P$ as premises, you can get $Q$ using have s₁: Q := disjunctive_syllogism ⟨p₁, p₂⟩.
• If you have $P \rightarrow Q$ and $P$ as premises, you can get $Q$ using have s₁: Q := modus_ponens ⟨p₁, p₂⟩.
• When you have $P \rightarrow Q$ and $\lnot Q$ as premises, you can get $\lnot P$ using have s₁: ¬P := modus_tollens ⟨p₁, p₂⟩.
• If you have $\lnot\lnot P$, use rw [double_negation] at p₁ to rewrite the premise as $P$.
• When you have $\lnot(P \land Q)$, use rw [de_morgans_and] at p₁ to get $\lnot P \lor \lnot Q$.
• If you have $\lnot(P \lor Q)$, use rw [de_morgans_or] at p₁ to get $\lnot P \land \lnot Q$.