- Automated vs. interactive theorem proving
- Decision procedures for real closed fields
- My project: an alternative approach
- Some philosophical comments

- They're accurate!
- They're fast!
- They can "comprehend huge problems" (in a certain sense).
- They can (sometimes) produce formal proofs.
- A standardized proof library is extremely useful.
- The math behind mechanized reasoning is interesting in its own right.

In automated reasoning, the computer attempts to solve a problem on its own, without input.

Examples: calculators, SAT solvers for boolean formulae

```
>>> s = Solver()
>>> s.add(Implies(p, q))
>>> s.add(Implies(q, r))
>>> s.add(p)
>>> s.add(Not(r))
>>> s.check()
unsat
```

In interactive theorem proving, the user gives "hints," and the computer fills in the gaps.

Examples: formalizations of prime number theorem, Kepler conjecture, homotopy type theory

These proofs often involve calls to automated tools.

```
theorem succ_le_succ {a b : Nat} (H : a + 1 ≤ b + 1) : a ≤ b
:=
obtain (x : Nat) (Hx : a + 1 + x = b + 1), from lt_elim H,
have H2 : a + x + 1 = b + 1, from (calc
a + x + 1 = a + (x + 1) : add_assoc _ _ _
... = a + (1 + x) : { add_comm x 1 }
... = a + 1 + x : symm (add_assoc _ _ _)
... = b + 1 : Hx),
have H3 : a + x = b, from (succ_inj H2),
show a ≤ b, from (le_intro H3)
```

My project sits near the intersection of these paradigms. It is an automated tool for a specific domain of problems, that frequently show up in interactive proofs.

If $0 < x < 1$ and $\ 0 < y < 1$, then $$ x^{500} + y^{500} > x^{500} \cdot y^{500} $$

This is a theorem in the theory of real closed fields: we are allowed constants $0$ and $1$, operations $+$ and $\cdot$, and repeated applications of these operations, and make comparisons using $>$ and $=$.

If $0 < x < 1$ and $\ 0 < y < 1$, then $$ x^{500} + y^{500} > x^{500} \cdot y^{500} $$

The theory of real closed fields is *decidable:* there is an algorithm that, given any sentence of this form, will determine whether it is provable or not. (Tarski, 1951)

But this algorithm is extremely inefficient! Its complexity doesn't correspond to any "intuitive" notion of difficulty.

And producing a proof certificate is even less efficient, by many orders of magnitude.

If $0 < f(z) < 1$ for all $z$, then $$ f(x)^{500} + f(y)^{500} > f(x)^{500} \cdot f(y)^{500} $$

It is also broken by any changes to the underlying language.

These shortcomings are disappointing:

- Heterogeneous problems in (simple extensions of) RCF are quite common across many fields of mathematics.
- They can be quite tedious to solve "manually" in interactive provers.

... and surprising:

- Restricted to just addition (or just multiplication), the theory becomes quite simple.
- Extensions of the language of RCF do not necessarily create structurally different terms.

If we accept the possibility that we will "overlook" proofs that depend essentially on distributivity, we can fix a number of these shortcomings, and get:

- Massive improvements in efficiency on a large class of problems
- Complexity that respects an "intuitive" idea of difficulty
- Easily constructible (and natural!) proof certificates
- Flexibility and extensibility

We call something that does this a *heuristic* procedure.

George Polya, known for his research in both problem-solving heuristics and in inequalities.

Polya consists of a collection of individualized "modules" that communicate with a central database. The database stores information in a shared language.

Given a collection of inequalities, Polya searches for a contradiction by the following steps:

- Convert each inequality into a standard
*normal form*. - Find all additive and multiplicative subterms and give them names.
- Iteratively run modules for additive and multiplicative arithmetic, to learn comparisons between these subterms.
- If the central database receives contradictory information, return "unsat".

Note: in classical logic, this is equivalent to proving a theorem from hypotheses.

$$y\cdot x \cdot x + \frac{1}{5}\cdot y^3\cdot z \cdot 5 \cdot x \cdot z < -x $$
becomes

$$\underbrace{\underbrace{x^2\cdot y}_{t_1} + \underbrace{x\cdot y^3\cdot z^2}_{t_2} + \underbrace{x}_{t_3}}_{t_4} < 0$$

Note that a comparison like $t_4 < 0$ is both additive and multiplicative!

If we take a set of purely additive (or multiplicative) equations and/or comparisons, we can use variable elimination to find new comparisons in the common language.

$$ t_3 + t_8 < t_5 \wedge t_3 > 0 \implies t_8 < t_5 $$

$$ t_9 = 3\cdot t_1^2 \wedge 0 < t_1 < 1 \implies t_9 < 3 $$

There are multiple ways to do this:

- Fourier-Motzkin variable elimination: simple, but can "blow up" in difficult cases
- Geometric methods: potentially better bounds on complexity, but more complicated

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

Suppose the following: \begin{align*} t_1 &< 3t_4 + t_7 \\ t_4 &< t_7 - 2t_5 \\ t_7 &< 8t_0 \\ t_7 &< -t_3 \\ 3t_5 &= 2t_1 + 2t_4 \end{align*}

We want to find comparisons between $t_1$ and $t_4$, so let's eliminate $t_7$.

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

First, rewrite everything so that $t_7$ is isolated: \begin{align*} t_1 - 3t_4 &< t_7 \\ t_4 + 2t_5 &< t_7 \\ t_7 &< 8t_0 \\ t_7 &< -t_3 \\ 3t_5 &= 2t_1 + 2t_4 \end{align*}

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

Now, split into three categories:

$t_1 - 3t_4 < t_7$ | $t_7 < 8t_0$ | $3t_5 = 2t_1 + 2t_4 $ |

$t_4 + 2t_5 < t_7$ | $t_7 < -t_3$ |

For every pair of inequalities, one from the first category and one from the second, we derive a new inequality in the third:

$t_1 - 3t_4 < t_7$ | $t_7 < 8t_0$ | $3t_5 = 2t_1 + 2t_4 $ |

$t_4 + 2t_5 < t_7$ | $t_7 < -t_3$ | $t_1 - 3t_4$ $<$ $-t_3$ |

We end up with the following set of inequalities, which are *equisatisfiable* to the original set:
\begin{align*}
t_1 - 3t_4 &< -t_3 \\
t_1 - 3t_4 &< 8t_0 \\
t_4 + 2t_5 &< -t_3 \\
t_4 + 2t_5 &< 8t_0 \\
3t_5 &= 2t_1 + 2t_4
\end{align*}

If we repeat this procedure to eliminate $t_0$, $t_3$, and $t_5$, we end up with \begin{align*} t_1 &> -\frac{2}{5}t_4 \\ t_1 &< -\frac{8}{3}t_4 \end{align*}

The multiplicative version of this algorithm works very similarly, with one notable sticking point: we need to know (or assume) the signs of terms.

(This is because the logarithm function is only defined on positive reals!)

There are inefficiencies in the Fourier-Motzkin procedure that would be nice to avoid.

An improvement to this procedure can be seen by interpreting matters geometrically.

With respect to variables $t_1,\ldots, t_n$, an equation $c_1t_1 + \ldots c_n t_n = 0$ defines an $(n-1)$-dimensional *hyperplane* through the origin in $\mathbb{R}^n$.

An inequality $c_1t_1 + \ldots c_n t_n < 0$ defines a *half-space* in $\mathbb{R}^n$.

A collection of inequalities of this form determine a *polytope* (an "infinite pyramid") with vertex at the origin.

We're interested in two dimensions at a time. So if we *project* the polytope to the $t_i t_j$ plane, we can read off the comparisons between $t_i$ and $t_j$ from the "shadow."

This projection is easy, if we convert the polytope to its *vertex representation* first.

But this conversion is hard!

In effect, converting the polytope to its V-rep does the entire Fourier-Motzkin routine at once, without (as much) redundancy.

But using external tools to do this is opaque, and it isn't entirely clear how to construct a proof certificate with this method.

No matter which arithmetical method we use, we derive the same facts about subterms of the original problem.

These facts lead us to an "unwinding" proof of the desired sentence, via simple inferences.

A contradiction is found when the modules find a subterm with inconsistent bounds: say, $t_5 > 3$ and $t_5 < 2$.

The decentralized structure makes it simple to extend the procedure to new types of terms.

A sentence of this form is "comprehensible" almost by default.

But we can do even more than comprehend it, by adding new modules.

Because of the architecture, new modules and new term structures can't interfere with the core arithmetical base.

One important module takes universal axioms from the user, of the form $$ (\forall x, y)(x < y \rightarrow f(x) < f(y)). $$

The module instantiates this axiom with respect to terms in the central database: if we have defined $t_3 = f(a)$ and $t_5=f(b)$, we will learn the clause $$a < b \to t_3 < t_5.$$

We want to *avoid* instantiating everything: if $f(a)$ doesn't show up in the problem, we shouldn't bother instantiating axioms that give information about $f(a)$.

But, we don't want to be too conservative: if $f(a)+f(b)$ is not a problem term, but $f(a)+f(b)+c$ is, an axiom that tells us about the former could be useful.

The solution: a balance, using *trigger terms*.

We'll allow the axioms to create new "terms of interest," as long as they're combinations of current terms in the problem.

This is, again, a *heuristic*!

We have additional modules planned for:

- Exponential and logarithmic functions: $$e^{t_1 + t_2} = e^{t_1}e^{t_2}$$
- Integer arithmetic: $$int(z)\implies \lceil z \rceil = z$$
- Second-order operators $$f(x)>1 \implies \int_a^b f(x) > b-a$$

We envision Polya as a complement to the standard automated methods available in interactive proof assistants.

There are some situations where the old methods are better, and some where ours is better!

Areas we can improve on:

- Implementing proof certificates
- Better case splitting and backtracking
- More modules for more domains
- More efficiency in general

What counts as a mathematical proof?

Traditionally, a proof is something that convinces mathematicians of the truth of a statement.

Proof-theoretically, a proof is a sequence of valid inferences in a specified deductive system.

In between, a proof is something that convinces mathematicians that such a deduction is possible in principle.

How do we recognize something as a mathematical proof?

- Peer reviewers?
- (Manual) formal deductions?
- Computer-verified proofs?

How do we recognize something as a formal deduction?

What does this say about the epistemic status of a proof-theoretic proof?