output the dependencies between theorems as a directed graph

Stream: Is there code for X?

[Asei Inoue]

I would like to create a roadmap for people learning mathematics that describes what to learn and in which order.

I have been manually drawing graphs with Mermaid, but I thought it would be useful to be able to generate some automatically.

Is it possible for Lean to output the dependencies of the theorems defined under a given namespace (i.e. the relationship that the proof of Theorem A is used in the proof of Theorem B)?

It would be of considerable educational significance if it were possible to automatically output a graph of dependencies.

[Trebor Huang]

Note that the logical dependency order is not necessarily the pedagogical dependency order. We do not learn real numbers after Cauchy sequences, quite the reverse!

[Kevin Buzzard]

Are you talking about learning the subject of mathematics, as opposed to learning anything to do with lean?

If so, I think there is ample evidence to suggest that learning it in the "right order" as specified by exactly what can be deduced from what, is not the way to learn mathematics. Sure the natural number game is fun, but proving that the integers are a commutative ordered ring is very tedious, proving that the rationals are an ordered field is very tedious, and if you try to learn maths this way you'll never even get to the real numbers. At university I was told on day 1 that the real numbers existed and satisfied the completeness property, and was told not to worry about it. This saves many hours of boring manipulations.

[Kevin Buzzard]

Where by "boring" I mean "I find them fascinating but I'm well aware from talking to people that I'm very much in the minority"

[Asei Inoue]

If you can output 'only the mutual dependencies of the theorems in a particular namespace', you can automatically output the dependencies of each theorem when you write a book in Lean.

[Asei Inoue]

@Kevin Buzzard @Trebor Huang wouldn't that be useful? It could also be a motivation to learn Lean.

[Kevin Buzzard]

Another example is that mathlib does single variable calculus after multivariable calculus which is only done after measure theory and the theory of topological vector spaces. No student learning the basics of calculus wants to see all that.

[Trebor Huang]

I agree that it is useful, but I would disagree that it is useful educationally.

[Asei Inoue]

If we restrict outputs to 'only certain namespaces', there should be no boring fundamental theory output.

[Kevin Buzzard]

Another example: the theory of finite groups is taught to first year undergraduates with no mention of the very thorny foundational set-up behind the theory of finiteness; statements such as "a finite set has a unique size which is a natural number" are regarded as obvious and no definition of finiteness is given. In mathlib we have literally many thousands of lines about multisets and finsets all of which are never taught and are probably of no pedagogical value at all to working mathematicians.

[Asei Inoue]

I assume that you are writing a maths textbook in Lean and outputting its dependencies.

[Asei Inoue]

The output of theorem dependencies in mathlib is certainly not educational. I agree with you.

[Kevin Buzzard]

I don't want to distract you from the kind of concrete questions you raise about automatically generating graphs and so on, which might have applications, but I believe that your claim that such a tool would be of "considerable educational significance" is naïve and not at all backed up by any theory of mathematical education, which suggests that the picture is far more complex.

[Asei Inoue]

@Kevin Buzzard I understood that it would not be very useful for education ... However, if it becomes possible, I would say that it would be one of the advantages of writing proofs in Lean instead of ”pencil and paper".

[Kevin Buzzard]

In fact those of us who have taught lean courses to mathematics undergraduates have had to wrestle with many problems, including the very complex interaction between the goals of "teaching students mathematics" and "teaching students lean". I personally have adopted the path of least resistance, where I let other people teach the mathematics in the traditional manner, and then I teach students lean assuming they already know the mathematics. People like Patrick Massot and Jeremy Avigad and Heather Macbeth have tried far more ambitious approaches but such courses are far more tricky to pull off.

[Asei Inoue]

Is it actually possible to output dependencies in Lean?

[Kevin Buzzard]

Yes, I'm sorry to derail your actual concrete question. I do not know the answer to this but it would not surprise me! It was the "considerable educational significance" claim which set me off.

[Asei Inoue]

@Trebor Huang @Kevin Buzzard I apologise for my ignorance of mathematics education. Thank you.

[Kevin Buzzard]

And I apologise for derailing your question!

[Asei Inoue]

I'd still like to do some graph output - didn't mathlib have a similar function as an existing feature?

Is this related?
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Util/Imports.html#Lean.Environment.importGraph

[Kevin Buzzard]

People who write mathematics projects create graphs like this https://leanprover-community.github.io/flt-regular/blueprint/dep_graph_document.html and there was a discussion about this here, but I don't know enough about the details to know if this is related to what you want.

[Asei Inoue]

@Kevin Buzzard Thank you!!

[Kevin Buzzard]

In particular I think that some aspects of that graph might be being generated manually rather than automatically

[Asei Inoue]

I think this is not made with mermaid.