# Rewrite Search

Sometimes you know things because of theorems whose form is, when you
know one true thing, then you know another true thing. `P`

implies `Q`

. If
`x`

is even, then `x^6`

is divisible by `64`

. And `10`

is even, therefore `10^6`

must be divisible by `64`

. Figuring out when this applies is the
“library search” problem I wrote about last month.

Rewrite search is a bit different. A rewrite happens when you know
that two different expressions are equal. So you can replace one of
those expressions with the other, inside a longer statement. `10^6`

equals a million. And `10^6`

is divisible by `64`

, so a million is
divisible by `64`

.

The basic “rewrite search” problem is, given two different expressions, figure out how to make them equal through a series of rewrites.

## Why is rewrite search important?

I think most “normal person mathematics” can be thought of as a series of rewrites.

Consider a question like “what are the factors of 27?” (I found this by googling “math question” and taking the first one that looked like a pure math question.)

The normal way to solve this is roughly, first you consider that ```
27 =
3^3
```

. Then you perhaps know that for a prime `p`

, the factors of `p^n`

are
`p^k`

for `k`

in `[0, n]`

. You can write a series of expressions like

```
factors(27)
factors(3^3)
3^k for k in [0, 3]
3^0, 3^1, 3^2, 3^3
1, 3, 9, 27
```

where each expression is a rewrite of the expression in the previous row.

There are a few more details here that make this not purely a
rewrite question. For example, we didn’t have a theorem for the
factors of `3^3`

specifically. We had a theorem for the factors of `p^n`

,
where `p`

was prime. So we need to be able to rewrite based on a
formula, and to apply some conditions to the formula. We need to know
that `3`

is prime, and that isn’t a “rewrite search” type of problem,
that’s a “library search” type of problem.

Another detail is that we didn’t start off with a particular
destination in mind. We didn’t have the problem of, rewrite
`factors(27)`

into `[1, 3, 9, 27]`

. We just wanted to rewrite `factors(27)`

in a simpler form.

Another detail is simplifying the “for loop”, which maybe happens in multiple steps.

That said, the essence of the problem is rewriting. Most questions of the form “solve for x” or “what does this expression evaluate to” are fundamentally about rewriting. As opposed to questions of the form “prove that X is true”, which are often more implicationy.

## What can we do about it?

orked on the Lean rewrite_search tactic for a while. It didn’t end up as useful as I had hoped. The main problem is that there are so many possible ways to rewrite a formula, you can’t use a plain breadth-first search and get very far. We need to be using AI heuristics. In Lean we were hoping to get mathematicians to tag theorems based on how good they were for rewriting, but this was just too much of a hurdle.

Intuitively, I think this makes sense, that we should have a heuristic
sense for how good expressions are to rewrite into other expressions.
You see `27`

in a math problem, you
immediately think that’s `3^3`

. You see `6401`

in a math problem, you
immediately think that’s `80^2 + 1`

. These potential rewrites move
forward in your mind, even if these numbers are just a small part of a
larger expression.

The other thing we need to do tactically is to be using rewrites
starting at every expression in a problem. A bidirectional
search. When
you’re searching for a path of length `2n`

from A to B, with a branching
factor of `b`

choices at each step, and you start just at A, you have to
search `O(b^2n)`

nodes. If you start forwards from A and backwards at B,
you only have to search `O(2b^n)`

nodes, which looks similar but is far
better.

## Conclusion

I think these two forms of reasoning, library search and rewrite search, plus basic propositional logic, are capable of solving a large amount of mathematics problems.

Now what? In a sense this has been a “bottom up” view, answering what tactics are useful for solving math problems. We also need a “top down” view. Can we build a math AI that starts with a narrow focus on a small set of math problems, nails that, and expands its domain of mastery over time? I’d like to write more on this topic next month.

Thanks for reading!