An idea to optimize and simplify proofs.

[marswill]

I was reading this thread the other day talking about optimizing the proofs generated by $\pi$-base.

I had an idea which I thought to post as a comment there, but it got kind of long-winded, and I didn't want to hijack @prabau 's thread with a long word-salad.

So instead I decided to hash out my ideas here, in a separate thread that can be safely muted :)

In the other thread, @jamesdabbs wrote:

Yeah, for each space, we broadly

• start with a queue of all theorems about the asserted traits
• repeatedly try to apply them to deduce new traits
• if we succeed, re-enqueue theorems related to the new property

There certainly may be more clever approaches we could take. Without a more clever approach, I'd assume it's computationally infeasible to try to find the minimal-size proof for every deducible trait globally. It seems more tractable to me to have a "find alternative proofs / simplify proof" view when looking at a particular trait.

What happens if you define the length of a deduction as the shortest number of complex theorems needed to prove the results? Here I consider a theorem of the form $A\implies B$ (or $A\implies \neg B$, or $\neg A \implies B$) to be simple, and all others complex.

The philosophy for this definition is that a long chain of simple implications $A\implies B\implies C \implies D$ is often artificial complexity, and many mathematicians probably don't need to even see the whole chain - a default view of a more complicated proof using such a chain could just show $A\implies D$, with a little "+" icon to expand the chain of equivalences for anyone who needed to see them.

I have a suspicion if you define things this way, and persistently store all the simple implications, then a breadth first search might be feasible.

I also have some ideas for how to implement this, though as I'm still digesting how the site works currently, maybe they should be taken with a grain of salt. In any case, I'll elaborate in a comment.

[marswill]

So here is the gist of how something like this might be implemented:

---

1.) persistently store the results of every simple ($A\implies B$) theorem, and their transitive closure. Record these in two places: a dictionary (e.g., key $T_4$, value $[T_3,T_2,T_1, T_2.5, US, KC, etc..]$), as well as a directed acyclic graph with properties as nodes, and simple theorems as directed edges.

2.) When you generate a proof something is impossible, you are trying to prove something like $\neg (P_1\wedge \dots\wedge P_n)$. So begin with not simply the list $P_1,\dots,P_n$ but rather the list of those properties and all simply derived properties.

Now you can do a breadth first search through the graph of all states of known of properties, joined by applicable theorems, to look for a contradictory state. (Note this is abstractly what you're doing, of course we don't need to store said graph anywhere. Every node in this graph could be represented pretty compactly as a $2N$-bit sequence, where $N$ is the total number of properties.) At every step, you add not only the concluded trait, but the list of ALL simply implied traits deducible from that trait (persistently stored in a dictionary per 1).

My hot take is it ought to be feasible. There are by my count about 150 complex theorems in $\pi$-base, but many will be permanently inapplicable*, and as more become applicable in each step, others become ruled out. My wild guess would be the number of applicable theorems at each step is probably in single or low double digits.

(*Every theorem is itself a negated conjunction, say e.g., $\neg(Q_1\wedge\dots\wedge Q_n)$. Once any of $Q_1,\dots,Q_n$ are known to be false the theorem is permanently inapplicable, if two or more traits are unknown and the rest are true, its inapplicable but might be applicable in the future, if all but one are known to be true it's applicable now, and if all are known to be true then we are at the end of the proof and have our contradiction.)

3.) After you get the list of theorems used in a shortest path, alongside the list of all "states of known properties" between each theorem, work backwards to generate the proof as follows:

• At the end of your deduction, you have deduced $Q$ and $\neg Q$ for some $Q$. Place those two in a "needs justification" list $L$.
• Since your deduction is a shortest path, the last theorem, $T_n$, concludes some property $P_n$, which generates property either $Q$ or $\neg Q$. WLOG say $P_n\implies Q$. From the acyclic graph in 1), find a shortest direct chain from $P_n$ to $Q$. Place that chain at the end of the proof. (only $P_n\implies Q$ need be visually displayed, unless user clicks the little plus icon mentioned earlier). Theorem $T_n$ itself is the second to last step of the proof.
• Since $T_n$ deduced $P_n$, $T_n$ has the form $\neg(\neg P_n \wedge P_n^1\wedge P_n^2\dots P_n^k)$, so remove $Q$ from the list $L$ and add $P_n^1$ through $P_n^k$.
• The conclusion $P_{n-1}$ of theorem $T_{n-1}$ will definitely generate at least one property from $L$, as otherwise $L$ was already known and $T_n$ could have been applied one step earlier. Create proofs via shortest direct chains for any such properties as before via the acyclic graph from 1). Place them between theorem $T_n$ and theorem $T_{n-1}$. Remove any of these properties from $L$, and replace them with properties $P_{n-1}^1,\dots P_{n-1}^k$, where $T_{n-1}=\neg(\neg P_{n-1}\wedge P_{n-1}^1\wedge\dots\wedge P_{n-1}^k)$.
• Continue in this fashion until you reach the beginning of your shortest path, and you have your proof.

4.) The breadth first search is obviously only important for generating proofs. For generating the list of properties of a single space you can do what it seems you already do, possibly slightly more efficiently: Just repeatedly applying theorems until no more are applicable, but still adding all of the persistently stored simply-implied properties after each theorem.

On the other hand, if it turns out to be efficient enough (and I suspect it might), generating a single shortest possible chain of deductions for a given space might also be valuable. One could do the breadth first search for the property generation as well, taking the shortest path to a state where no theorems are applicable. This could give a user a nice overview on the main page of a space for how all the important properties are deduced - again only showing the strongest properties deduced and the complex theorems used, and hiding the rest inside chains of simple deductions, that can be expanded by users if more detail is desired.

[prabau]

Just to make things clear, each of the $P_i$ and $Q_i$ above is either a property, or the negation of a property, right?

[marswill]

Yes.