The Goal of Mechanize Math

Machines have become increasingly valuable in the field of math. They have been used to perform massive combinatorial calculations, churn through symbolic computations, and even prove some complicated theorems.

The class of problems computers excel at are those that can be solved procedurally. Indeed, computation is all about rigidly following procedures. But so far only certain math problems have fallen into this domain.

The aim of the Mechanize Math project is to massively expand the class of problems that can be solved via computation. I wish to define a procedure that outputs answers to any math/logic problem that can be solved with pure reason. Granted, this is a massive goal.

A natural question is whether such a goal is even possible. While I can’t say for certain, my intuition is that it is. Math is a highly logical domain (some say it’s pure logic) and computers excel at logical computations. Additionally, the experience of doing math already feels highly procedural. Many proof steps are completely forced by the problem statement, to the point where one can almost imagine a computer performing them.

Granted, sometimes a proof is cracked by a step that feels as though it was pulled from thin air. These bursts of intuition feel like pure human creativity, impossible to replicate by machine. But oftentimes if you think a little more carefully, you can trace the thought pattern that produced these insights. The notion of an idea coming out of nowhere seems unfathomable.

But even if I’m wrong, it seems highly worthwhile to at least attempt to find a procedure for “mechanizing” math. Worst case is that this fails and in the process we learn a lot of interesting stuff about mathematics, computation and the human mind.

So we continue with the assumption that a procedure for solving all math problems exist, and we simply need to find it.

The Problem, Stated Formally

The goal is to define a procedure that can solve any math/logic problem solvable with pure reason.

By procedure, I refer to the Church/Turing sense of the word, where a well-defined procedure is anything that can be represented with a Turing machine. This is the highest level of rigor possible in defining a procedure, and ensures that any computer will be able to perform the steps necessary to solve the math/logic problem.

I specify problems solvable by pure reason to explicitly not include two classes of problems:

1. Problems that rely on empirical data
2. Problems that are ambiguous.

The first class of problems is pretty easily identifiable. However, determining when a problem is ambiguous is, ironically enough, somewhat ambiguous. Intuitively, it is unreasonable to expect a program to determine the logical truth of statements that contain undefined terms and other ambiguities. But how exactly to identify and handle these ambiguities is a central goal of the project. Ideally, a program would be intelligent enough to communicate to the user where ambiguities lie and invite them to offer clarifications.

Inputs and Outputs

Many automated theorem provers force inputs to adhere to a formal language like First Order Logic or Type Theory. The benefit of this is that the restriction forces inputs to be logical and unambiguous. A sentence in Type Theory cannot express an emotion or opinion, or any other non-logical idea.

However, I will not be limiting the domain to a formal language. Our definition-of-done will not be satisfied until the system is capable of handling natural language inputs.

The reason for this is that humans do not think or state ideas in a formal language, we reason in something that’s much closer to natural language. Even if I did restrict myself to a type theory, the question would always remain, now how do we build a program that formalizes the natural language into the type theory. So in the spirit of being maximally ambitious, we will force our input to be natural language.

That is not to say that our system can’t employ formal languages in its internal processing. Indeed, I think it’s quite likely that such a move is necessary. But we shouldn’t let that restrict the input form. Instead, we should think deeply about what it means to faithfully formalize from Natural Language into formal language.

Soundness and Completeness

In addition to everything mentioned above, one other thing is necessary for our definition-of-done: reasonable confidence that our procedure is sound and complete.

By soundness, I mean that our procedure will never prove something false. By complete, I mean that if a solution to a problem exists, our procedure will eventually find it (even if it has to run forever).

Soundness and completeness have a precise definition and can often be formally proved. I don’t think it will be possible to “prove” it for our system (unless we specify some arbitrary language from which to prove it), but nonetheless we should have reasonable confidence that the two properties hold.

This requirement is critical. We must be confident that we are finding a procedure that will not fail us ever. Otherwise, the question will always remain of how to define a system that doesn’t fail.

The Approach

Of course, this problem is utterly gigantic. Solving it would quite possibly be the biggest advancement in AI ever. But I do think it is decomposing to several sub-problems. I also think that the process of finding a solution itself will be incredibly informative on a number of other questions.

Pertinent Questions

Here are a list of questions (in no specific order) that I think are relevant to finding the procedure. I hope they will guide the process.

1. What does it mean to “faithfully formalize”a statement from natural language into a formal language.
2. How do we reason about the expressivity of a formal language? How do we know if a language is expressive enough to represent whatever math concept we wish to express?
3. How do we identify and handle ambiguities in natural language? Can we create a sub-procedure that determines if a natural language problem statement is ambiguous?
4. When a human proves something, which proof steps are forced, which are a search procedure, and which are out of thin air? Can these “out of thin air” steps always be show to be forced in some way?
5. Can we define a language for representing the process of searching for a proof, in the same way we have formal languages to represent both theorems and proofs?
6. How do we know when a proof is rigorous enough?

Why Now?

Unfortunately, a lot of the information needed to solve this problem is trapped in disparate domains. The central question taps into questions across math, logic, formal methods, theoretical computer science, PL theory, and philosophy. Academia has unfortunately organized itself such that few people are studying these fields together.

However, I see three modern occurrences that make the present the perfect time to embark on this project.

1. The significant advancement of formal methods. We now have tried and tested systems for representing theorems and proofs to a computer. Such a system would’ve been unthinkable even 100 years ago. Libraries like Mathlib are collecting a growing corpus of formalized math, which is also a great domain for testing automated theorem proving techniques.
2. Advancements in natural language processing and large language models. Building functions that intelligently go from NL input to NL output is far better understood.
3. The increases in productivity and access to information created by consumer LLM products. It’s finally possible to write complex code bases and search through hundreds of papers with minimal effort. This is transformative in this domain as it is in any other.