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?