-3
$\begingroup$

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?

Improve this question
$\endgroup$
8
  • 1
    $\begingroup$ Similar techniques are thoroughly investigated in theorem provers a few decades ago. $\endgroup$
    – Trebor ♦
    Oct 3, 2022 at 10:21
  • 5
    $\begingroup$ 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. $\endgroup$
    – Couchy ♦
    Oct 3, 2022 at 14:53
  • 1
    $\begingroup$ 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... $\endgroup$
    – user1168
    Oct 3, 2022 at 17:44
  • 1
    $\begingroup$ @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. $\endgroup$
    – Meven Lennon-Bertrand
    Oct 4, 2022 at 15:40
  • 1
    $\begingroup$ @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 $\endgroup$
    – Couchy ♦
    Oct 5, 2022 at 1:29

1 Answer 1

Reset to default
5
$\begingroup$

Building that gigantic proof graph as an explicit graph would probably be a very bad idea, given its size and the complexity of "connecting inputs to outputs". Indeed, as you can have an arbitrary substitution in-between, which triggers computation, said connection in effect corresponds to the undecidable problem of higher-order unification. And even adopting simple heuristics and accepting to lose some solutions will have a very high time cost, given the size of libraries such as Lean’s Matlib or Coq’s Mathematical Components.

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – Daniel Donnelly
    Oct 3, 2022 at 9:56
  • $\begingroup$ Please explain more: " Indeed, as you can have an arbitrary substitution in-between, which triggers computation, said connection in effect corresponds to the undecidable problem of higher-order unification." I'm not sure what you mean with regard to what I said. For example, what do you mean by "arbitrary subst. in between that triggers computation"? $\endgroup$
    – Daniel Donnelly
    Oct 3, 2022 at 10:02
  • $\begingroup$ I don't think it's faster and as comprehensive to do graph generation on-the-fly as you mentioned Coq does. If you had the graph already compiled, then you're likely to get a speed-up as long as you can fit it into memory. If you can't fit it into memory, then offer it as a super-computing service in the cloud. $\endgroup$
    – Daniel Donnelly
    Oct 3, 2022 at 10:08
  • 1
    $\begingroup$ 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). $\endgroup$
    – Meven Lennon-Bertrand
    Oct 4, 2022 at 15:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.