Making a computer solve your math problems
Chase Norman: “If there exists a proof, we’ll eventually find a proof of that statement.”
Sometimes, all you need to do to get over a roadblock in a math proof is to think about the problem in a different way. This was the inspiration behind Chase Norman’s automated math problem solver.
On Nov. 19, Norman, a PhD student at Carnegie Mellon University, presented Canonical, his theorem prover, at a talk organized by the student group AI@MIT.
Canonical is built on top of a mathematical proof assistant called Lean, which automatically checks if a sequence of math statements (“tactics”) written in the Lean programming language correctly proves a statement.
When a person proves a theorem, they typically present a sequence of logical steps. If each step is valid, they together establish the truth of the original statement. For instance, someone might show that each angle in an equilateral triangle is 60 degrees by observing that the sum of the angles in a triangle is 180 degrees, the three angles are the same, and that 180 divided by 3 is 60.
According to Norman, Lean verifies proofs in a similar way. It begins with compiling tactics into standardized proofs (“terms”). Each term attempts to prove a logical proposition (belonging to a “type”). Lean verifies that a term is correct (or “typecheck” each term), and ultimately returns if any term belongs to the type of the original theorem.
“Another advantage of automated theorem proving is that there is a formal definition of a mathematical proof and there’s a way to verify whether the proof is correct or incorrect,” Norman said.
Norman’s main insight was that mathematicians rarely solve hard problems by repeatedly coming up with brilliant intuitions and writing out terms. Rather, an important part of problem-solving is breaking down a complex task into smaller, more manageable types or transforming it into a more tractable form.
Norman referenced a seminar from Fields Medal-winning mathematician Terence Tao: “If you can find the right state in C — which is halfway between A and B — and each of those steps is half as difficult, that is a major, major advance.”
Programmatically, Lean enables this strategy of searching for the right intermediate states via computational tactics on propositions. Norman divided these operations into three main categories: closers, which will instantly prove a type if possible; simplifications, which rewrite a proposition into something easier to work with if possible; and transformation tactics, which change a type into a related proposition. He chose to let Canonical try all possible closers and simplifications, and then focus on the transformations.
“There’s not that many [closures or simplifications]. They don’t take that long to run. If they succeed, then you’ve made the goal simpler,” Norman said.
For his final insight, Norman observed that all proof transformations, no matter how complex, have three steps: creating a new subgoal, proving this tool is mathematically legal, and using it to complete the original proof. In the equilateral triangle example, a person might first reduce the original problem to the task of showing that the angles in an equilateral triangle are the same, and using this tool to show that each angle is 60 degrees. In Lean, a have function defines a subgoal. So, Norman could replicate all techniques available in Lean only using have statements.
Canonical puts all of these insights together. Given a goal claim (represented as a type), Canonical begins by creating a placeholder term for the proof. It then systematically refines this term through successive steps, exploring different transformations until it discovers a reduction that satisfies the goal.
“If there exists a proof, we’ll eventually find a proof of that statement. And our guarantee of Canonical is that if there is a short proof, then we can find that proof relatively quickly,” Norman said.
In the future, Norman hopes that incorporating artificial intelligence (AI) will enable Canonical to think about a problem from many different angles. One current challenge of Lean is recognizing separate representations of the same concept. For instance, a human can understand a positive number as its distance from zero and as its prime factor decomposition, but these two representations are programmatically very different. Norman envisions that AI tools, with their ability to interpret meaning rather than syntax alone, could bridge this gap and expand the capabilities of automated theorem proving.
“You no longer need to reason about terms. You can just reason about types. You no longer need to reason about any other tactics, even. And now, in order to take this one level of abstraction higher, I think the way to do it is with artificial intelligence,” Norman said.