# Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?

So I'm not sure how things are done in Lean4 or Coq, but I'm interested in their search features. For example, "Search for all theorems that get satisfied given a user-defined list of assumptions".

Couldn't you have theorems be nodes with a number of input assumptions, if another node is connected to a certain input, then the output of that node is the assumption (up to consistent variable / operator substitution).

So it's a lot like the concept of a Proof Tree, except cycles are allowed. After all, "If $$a,b \in A$$, then $$a + b \in A$$ has an output that can be plugged back into the theorem or magma definition itself.

Anyway, how search would work is you'd "light up" some nodes that are assumptions, these in turn light up the nodes pointed to by this node, as long as the full set of inputs of the next node becomes satisfied. And so on... (you repeat this until no more activations happen). So if you visualized this graph that covers a large body of math, then it will appear to look like a signal propogating through a brain's synapses.

Anyway, I hope I explained everything well enough. So essentially, just think Proof/Theorem Graph, instead of the more restrictive notion of Proof Tree.

I'm wondering, does this have the potential to speed up ATP (automated theorem proving) or ATD (automated theorem discovery) type systems? Or are they already doing something that outperforms this method?

• Similar techniques are thoroughly investigated in theorem provers a few decades ago.
– Trebor
Oct 3, 2022 at 10:21
• Saturation theorem provers already work in this way, the issue is not the algorithms we use for ATP, but the unavoidable fact that ATP is NP complete. We will never find efficient algorithms for theorem proving.
– Couchy
Oct 3, 2022 at 14:53
• This question makes me wonder about theorem proving on GPUs or quantum computers, but I need to learn alot more before I can ask my own question intelligently. It's been slow going...
– user1168
Oct 3, 2022 at 17:44
• @Couchy SAT-solving is NP-complete, but once you add quantifiers to the mix many problems become much harder, when they aren't simply undecidable. Oct 4, 2022 at 15:40
• @MevenLennon-Bertrand, I guess I should have clarified what I mean by the problem "theorem proving". If I refer to the language of derivable statements, then this is NP-complete, but if I say the language of valid statements then this indeed becomes undecidable
– Couchy
Oct 5, 2022 at 1:29

However, most basic automation/proof search (for instance auto in Coq) do something quite similar to what you suggest. They try and build a proof tree from the lemmas they have been instructed to use by repeatedly unifying the result of a lemma with the current goal, and then recursively trying to solve the premises. In a way, this is an implicit exploration of the graph you propose to build, done on the fly when asked to solve a particular goal.
• Here's related answer I made to another user's question: proofassistants.stackexchange.com/a/1773/548 which explains more of what I'm talking about. I think it might be faster than you think. If there are 23,000 theorems in MetaMath, e.g., then maximally there are 23,000 squared possible connections of a certain type (for example input/output connections). Not to mention, the node $f \text{ mono}$ is unique! It's the connections that specify the different references to / usages of that assertion. Oct 3, 2022 at 9:56
• Say you have a Coq lemma for commutativity of addition, and your goal is S n = n + 1. You can apply the lemma, by specializing it with n and 1, because 1 + n = n + 1 is convertible to the original goal. But to do so there is some computation involved (here, addition). In general, this computation can be arbitrarily complex, and so not only are there many involved ways to connect lemma inputs and outputs, but even deciding given two lemmas whether they "connect" is already a non-trivial task (and indeed, an undecidable one, this is the higher-order unification problem I mention). Oct 4, 2022 at 15:46