Hypergraph structure

Stream: general

[Ning Bao]

hi, i have a question about feasibility/utility of extracting a hypergraph data structure from Lean; does anyone more familiar with Lean have the time/inclination for a dm/call?

[Johan Commelin]

What exactly do you mean with "extracting a hypergraph"?

[Ning Bao]

I mean i'm envisioning a directed hypergraph where the theorem being proven is the sink, and the source vertices are the pieces needed to prove it

[Ning Bao]

this defines a directed hyperedge, and then assembling all of them together yields a graph

[Ning Bao]

i'm wondering if there's any additional utility conveyed by this data structure over just the dependency graph

[Snir Broshi]

As for utility I think there isn't much, unless you're doing it for a single file only.
For comparison here's the DAG of imports in Mathlib: https://leanprover-community.github.io/mathlib4_docs/mathlib.html
I find it hard to extract information from such a big graph

[Ning Bao]

interesting, can you explain a bit more why there's not much? I'm envisioning that a bunch of for example graph search algorithms could be applied to this sort of structure, and might yield interesting results

[Snir Broshi]

Ning Bao said:

interesting, can you explain a bit more why there's not much?

I explained in the message above, I don't think there's more to add

[Snir Broshi]

Basically I find the graph big and useless, but I find it cool - I'd print the Mathlib import graph and hang it somewhere.
The import graph can be used to optimize Mathlib's build time though.

[Ning Bao]

So you think there's nothing to be learned by running graph algorithms on it?

[Snir Broshi]

I don't know, what do you have in mind? The question is pretty vague, if you have a cool idea I'd love to hear

[Ning Bao]

I was wondering if you could say take a set of sources and determine which sinks are reachable

[Ning Bao]

or use the graph to determine bottleneck results between fields

[Ning Bao]

or use it as a proof conjecture generator, where it can help suggest which sets of lemmas form a minimal likely useful set for proving a targeted result

[Snir Broshi]

"which sinks are reachable" sounds like "find which theorems follow from a set of theorems", which is an undecidable problem

[Ning Bao]

or djikstra style search for finding shorter proof pathways

[Ning Bao]

that problem is only undecidable if you have the full representation of all math

[Snir Broshi]

But in general I think any huge graph can be made useful by adding some way to search it, e.g.
https://leanprover-community.github.io/queueboard/dependency_dashboard.html

[Ning Bao]

it's certainly decideable if you have a finite number of theorems

[Snir Broshi]

Ning Bao said:

that problem is only undecidable if you have the full representation of all math

I don't understand what you mean

[Ning Bao]

mathlib has a finite number of theorems

[Snir Broshi]

Ning Bao said:

it's certainly decideable if you have a finite number of theorems

It is not

[Ning Bao]

really? if i only have 2 theorems, one of which implies the other

[Ning Bao]

then the problem i posed is certainly decideable

[Snir Broshi]

As long as proofs can be arbitrarily long, and you're asking for a proof search rather than checking what theorems are used in the existing proof, then it's undecidable

[Snir Broshi]

Ning Bao said:

then the problem i posed is certainly decideable

It isn't unless I'm misunderstanding the problem statement (which I think I am)

[Ning Bao]

i'm just imagining doing a reachability analysis on a directed hypergraph where i have a set of marked vertices and i ask what vertices are reachable

[Ning Bao]

i'm not trying to violate godel

[Snir Broshi]

Oh so you're asking about the existing proofs and not which theorems can prove others.
Okay, then I have no idea what you mean by:

Ning Bao said:

or use it as a proof conjecture generator, where it can help suggest which sets of lemmas form a minimal likely useful set for proving a targeted result

[Ning Bao]

yeah so here it would be asking what additional vertex/vertices with which connectivity would allow a new result to be proven

[Ning Bao]

e.g. maybe theorem A is reachable from vertices X and Y and theorem B is reachable from X, Y, and Z

[Snir Broshi]

As long as you're talking about a "new result", your question becomes undecidable.

[Ning Bao]

well i don't think the hypergraph gives you the proof, it doesn't have enough type structure to do that

[Ning Bao]

but it could give you a sense of what types of results to attempt to prove

[Snir Broshi]

I don't understand what you mean, can you provide a concrete example?

[Ning Bao]

yeah, i'm not sure i can. it's hard for me to visualize what would or wouldn't be feasible with this data structure without building it and trying, so it's possible that this particular direction doesn't make sense

[Snir Broshi]

#metaprogramming / tactics > Theorem-level dependency graph