A tool to verify estimates, II: a flexible proof assistant

In a recent post, I talked about a proof of concept tool to verify estimates automatically. Since that post, I have overhauled the tool twice: first to turn it into a rudimentary proof assistant that could also handle some propositional logic; and second into a much more flexible proof assistant (deliberately designed to mimic the Lean proof assistant in several key aspects) that is also powered by the extensive Python package sympy for symbolic algebra, following the feedback from previous commenters. This I think is now a stable framework with which one can extend the tool much further; my initial aim was just to automate (or semi-automate) the proving of asymptotic estimates involving scalar functions, but in principle one could keep adding tactics, new sympy types, and lemmas to the tool to handle a very broad range of other mathematical tasks as well.

The current version of the proof assistant can be found here. (As with my previous coding, I ended up relying heavily on large language model assistance to understand some of the finer points of Python and sympy, with the autocomplete feature of Github Copilot being particularly useful.) While the tool can support fully automated proofs, I have decided to focus more for now on semi-automated interactive proofs, where the human user supplies high-level “tactics” that the proof assistant then performs the necessary calculations for, until the proof is completed.

It’s easiest to explain how the proof assistant works with examples. Right now I have implemented the assistant to work inside the interactive mode of Python, in which one enters Python commands one at a time. (Readers from my generation may be familiar with text adventure games, which have a broadly similar interface.) I would be interested developing at some point a graphical user interface for the tool, but for prototype purposes, the Python interactive version suffices. (One can also run the proof assistant within a Python script, of course.)

After downloading the relevant files, one can launch the proof assistant inside Python by typing from main import * and then loading one of the pre-made exercises. Here is one such exercise:

>>> from main import *
>>> p = linarith_exercise()
Starting proof.  Current proof state:
x: pos_real
y: pos_real
z: pos_real
h1: x 

This is the proof assistant’s formalization of the following problem: If are positive reals such that and $y

The way the proof assistant works is that one directs the assistant to use various “tactics” to simplify the problem until it is solved. In this case, the problem can be solved by linear arithmetic, as formalize dby the Linarith() tactic:

>>> p.use(Linarith())
Goal solved by linear arithmetic!
Proof complete!

If instead one wanted a bit more detail on how the linear arithmetic worked, one could have run this tactic instead with a verbose flag:

>>> p.use(Linarith(verbose=true))
Checking feasibility of the following inequalities:
1*z > 0
1*x + -7*z >= 2
1*y + -3*z  0
1*x > 0
1*x + -2*y  0 multiplied by 1/4
1*x + -7*z >= 2 multiplied by 1/4
1*y + -3*z 

Sometimes, the proof involves case splitting, and then the final proof has the structure of a tree. Here is one example, where the task is to show that the hypotheses and $(y>-2) \wedge (y-3) \wedge (x+y:

>>> from main import *
>>> p = split_exercise()
Starting proof.  Current proof state:
x: real
y: real
h1: (x > -1) & (x  -2) & (y  -3) & (x + y >> p.use(SplitHyp("h1"))
Decomposing h1: (x > -1) & (x  -1, x >> p.use(SplitHyp("h2"))
Decomposing h2: (y > -2) & (y  -2, y >> p.use(SplitGoal())
Split into conjunctions: x + y > -3, x + y >> p.use(Linarith())
Goal solved by linear arithmetic!
1 goal remaining.
>>> p.use(Linarith())
Goal solved by linear arithmetic!
Proof complete!
>>> print(p.proof())
example (x: real) (y: real) (h1: (x > -1) & (x  -2) & (y  -3) & (x + y 

Here at the end we gave a “pseudo-Lean” description of the proof in terms of the three tactics used: a tactic cases h1 to case split on the hypothesis h1, followed by two applications of the simp_all tactic to simplify in each of the two cases.

The tool supports asymptotic estimation. I found a way to implement the order of magnitude formalism from the previous post within sympy. It turns out that sympy, in some sense, already natively implements nonstandard analysis: its symbolic variables have an is_number flag which basically corresponds to the concept of a “standard” number in nonstandard analysis. For instance, the sympy version S(3) of the number 3 has S(3).is_number == True and so is standard, whereas an integer variable n = Symbol("n", integer=true) has n.is_number == False and so is nonstandard. Within sympy, I was able to construct orders of magnitude Theta(X) of various (positive) expressions X, with the property that Theta(n)=Theta(1) if n is a standard number, and use this concept to then define asymptotic estimates such as $X \lesssim Y$ (implemented as lesssim(X,Y)). One can then apply a logarithmic form of linear arithmetic to then automatically verify some asymptotic estimates. Here is a simple example, in which one is given a positive integer and positive reals such that and , and the task is to conclude that :

>>> p = loglinarith_exercise()
Starting proof.  Current proof state:
N: pos_int
x: pos_real
y: pos_real
h1: x >> p.use(LogLinarith(verbose=True))
Checking feasibility of the following inequalities:
Theta(N)**1 >= Theta(1)
Theta(x)**1 * Theta(N)**-2  Theta(1)
Infeasible by multiplying the following:
Theta(N)**1 >= Theta(1) raised to power 1
Theta(x)**1 * Theta(N)**-2  Theta(1) raised to power 1
Proof complete!

One challenge right now is that the logarithmic linear programming solver is not currently well equipped to handle “max” type expressions, thus for instance adding some lower order terms (specifically, asking whether and implies ) currently prevents this tactic from “one-shotting” the problem:

>>> p = loglinarith_hard_exercise()
Starting proof.  Current proof state:
N: pos_int
x: pos_real
y: pos_real
h1: x >> p.use(LogLinarith(verbose=True))
Checking feasibility of the following inequalities:
Theta(x)**1 * Max(Theta(1), Theta(N)**2)**-1  Theta(1)
Theta(y)**1 * Max(Theta(1), Theta(N))**-1 = Theta(1)
Feasible with the following values, for an unbounded order of magnitude X:
Theta(y) = X**0
Theta(x) = X**1/2
Max(Theta(1), Theta(N)**2) = X**1/2
Theta(N) = X**0
Max(Theta(1), Theta(N)) = X**0

Currently, LogLinarith() treats maxima such as Max(Theta(1), Theta(N)) and Max(Theta(1), Theta(N)**2) as variables independent of Theta(N), and thus misses some key (nonlinear) relations between these quantities that would allow one to prove the claim by contradiction. Currently I can prove this result within my proof assistant by a lengthier application of further tactics, but I plan to develop a more powerful version of LogLinarith() that performs the necessary case splitting to properly handle Max type terms to be able to “one-shot” problems such as the one above.

After that, I plan to start developing tools for estimating function space norms of symbolic functions, for instance creating tactics to deploy lemmas such as Holder’s inequality and the Sobolev embedding inequality. It looks like the sympy framework is flexible enough to allow for creating further object classes for these sorts of objects. (Right now, I only have one proof-of-concept lemma to illustrate the framework, the arithmetic mean-geometric mean lemma.)

I am satisfied enough with the basic framework of this proof assistant that I would be open to further suggestions or contributions of new features, for instance by introducing new data types, lemmas, and tactics, or by contributing example problems that ought to be easily solvable by such an assistant, but are currently beyond its ability, for instance due to the lack of appropriate tactics and lemmas.