Is it possible to map dependencies of theorems?

Stream: new members

[Dan Abramov]

I was chatting to @Kevin Buzzard a few weeks ago about the "blueprint" thing and how it relies on a bunch of manual work to keep up-to-date. Since that point, I've been wondering about something.

How difficult would it be to have a tool that can automatically map dependencies between theorems, and generate something akin to a blueprint? I don't mean including all theorems (since that would lead to a crazy explosion). But I was imagining some opt-in like

@[blueprint_node]
theorem some_theorem : blabla := by ...

And then theorems with @[blueprint_node] get automatically pulled into the visualization, with the graph representing which proofs depend on validity of which proofs. Theorems without the annotation are still considered in the relationship graph but don't appear as explicit nodes (so it's like they're "transparent" and only the transitive relationships between @[blueprint_node]s are visible).

So maybe you run some tool like ./generate-graph MyFile.lean and it finds all @[blueprint_node]s recursively and emits some HTML. Maybe there's also some way to break them into different pages, to generate LaTeX from docstrings, or whatever. The main idea is just that the source of truth is the code itself.

My question is

1) Whether this idea is bad in some way.
2) How feasible is something like this with today's Lean metaprogramming facilities. Would anything get in the way? Is this a couple days, a couple weeks, or a couple months of implementation work?

[Ruben Van de Velde]

The main use of a blueprint is before you have the formal proofs to derive the dependencies from, though

[Dan Abramov]

Hmm yeah.. Makes sense :man_facepalming:

Maybe there is a middle ground between having sorrys and working proofs? The main advantage I'm thinking of is that the system is driven entirely by code. Even if the actual proofs are duds waiting to be filled in.

For example, you could have something like

@[blueprint_node]
def theorem1 param1 param2 : blabla := by
  sorry

@[blueprint_node]
def theorem2 : blabla := by
  have := theorem1 sorry sorry
  sorry

Some nodes can then gradually start to get filled out, while the blueprint is responsive to those changes. As collision with the "real world" inevitably changes some of the graph, it automatically gets updated.

[Ruben Van de Velde]

Okay, but what if you haven't formalized the statement of theorem1? :)

[Dan Abramov]

That can still be a dud with just a name, right?

[Dan Abramov]

And a docstring.

[Dan Abramov]

So you can start with nodes that are sorrys all over the place but express the dependency between them in code by have := with sorrys as arguments. This gets you the initial blueprint with relationships. Then you can start filling it out in any order, slowly fleshing out the bits inside. As the shape changes or proofs actually get proven, all arrows are updated in sync with the code.

[Ruben Van de Velde]

It does sound interesting, but I wonder how well it would work in practice

[Dan Abramov]

Yeah, I don't know! The best way to find out may be to just try it, hence the second question — how "close" is this to doable with Lean's metaprogramming? If it's not an insane amount of work, I might as well try this to learn some Lean. But if it's very "against the grain" of how Lean works, it may not be the best idea.