Weights on dependency graphs

Stream: general

[Simone Melchiorre Chiarello]

Hi all. Apologize if the question is vague, but I'm curious to know whether it would be feasible / interesting to put weights in a "non-trivial" way on a dependency graph of a theorem or of a theory, and on operations on such graph. The inspiration for this comes from Google Scholar, which uses various metrics to rank publications and authors.

I was thinking of something like this (hand-wavy!): let T = (V,E) be a connected directed graph representing a theory, for example Algebraic Topology. Here each node is a theorem and two nodes e = (V1,V2) are linked if there is a proof available in Lean (so not if there exists, theoretically, a proof) which uses V1 as one of the hypotheses to prove V2. For instance, we can have V2 as the theorem that the fundamental group of S^1 is Z, and as V1 the homotopy lifting lemma for universal covers. We can then define the weight w(e) in various ways, say the lines of codes for the proof involving V1 and V2, or any other way in proof complexity theory (not very important here: let's just fix one).
Then, fixing a start node V0 (say ZFC) we can define the weight of any node V by calculating the path of least weight connecting V0 and V.

Now, an operation on this graph is any act expanding T to a graph T' including T. For instance, one could find a new proof for V2 (for example using Hurewicz theorem, homology, and the group structure on S^1) which amounts to add edges on T. Or one can add a node by simply proving a new theorem. I do not considering operations shrinking the graph since it's assumed that all proofs are correct and theorems do not "disappear", but I am free to have criticism on this.

Then we can rank an operation. For instance, after adding an edge, we can check the total difference of node weights between T' and T (I would imagine that reducing a node weight is better, since it amounts to finding a "simpler" proof of the same statement). Or after adding a node, we can calculate the weight of the nodes reachable from this new node (this metric of course changes with time), a high value meaning that the new node has been "cited" many times for new theorems.

This is just a vague idea and like that, it's probably ill-posed: does anything similar exist already? Can it be made rigorous?

[Johan Commelin]

I've dreamed about this quite a bit. But unfortunately I never came up with something useful that matches my personal taste/intuition about which pieces of maths are important or beautiful, or whatever.

[Simone Melchiorre Chiarello]

hi Johan and thanks for answering. Actually the idea was not to give a definition of importance of beauty (although it can serve as an inspiration), just to imitate objective metrics like Google Scholar does. These metrics do not coincide with importance or beauty of course, but they have the advantage of being definable :). Graph theory is surely applicable without talking about beauty, it just needs to be well-defined to avoid logical culprits.

[Oliver Nash]

I have also mused about this sort of thing and like Johan have never been able to convince myself to implement something but I'd certainly be interested to see anything that you build.

[Johan Commelin]

But you run the risk that you end up with metrics that do more harm than good. Just like all those crazy publication indices and metrics in academia that we all despise.

[Simone Melchiorre Chiarello]

That's a very interesting comment and it all comes to the goal of such metrics. Beyond GS (which is just an inspiration) I think that complexity theory on such system is something that naturally pops out, sooner or later: especially if the system increases in size significantly, having a better understanding on how complex this system is and reduce its complexity would be a worthy task.

[Johan Commelin]

Yes, that I agree with

[Scott Morrison]

Metrics that actually align with human notions of importance and/or beauty will of course be helpful when LLMs start making PRs...