Navigating mathlib4: How to build a mini-mathlib

Stream: mathlib4

[Shaonan Wu]

Dear all,
I am a new user of mathlib4 and my background is in computer science rather than mathematics. I would like to find the undergraduate-level theorems related to a specific mathematical field, such as algebra or number theory, in mathlib4. Could you please guide me on how to navigate through mathlib4 and locate the required theorems? I find it that the entire mathlib4 library is a bit complex to find what I need.
Thank you in advance for your assistance.

[Johan Commelin]

Does docs/undergrad.yaml help a bit?

[Johan Commelin]

There is also a rendered version on the website

[Johan Commelin]

https://leanprover-community.github.io/undergrad.html

[Shaonan Wu]

Johan Commelin said:

Does docs/undergrad.yaml help a bit?

Thank you. It really helps.

[Chris Wong]

That page seems to omit a couple things, like computability and graph theory. Should they be added?

[Johan Commelin]

@Chris Wong please add such things to https://leanprover-community.github.io/mathlib-overview.html

The undergrad.yaml is quite strictly aligned with the French undergrad curriculum (see note at the top of the page). And I think there is some value in that, because it provides an "external benchmark".

[Shaonan Wu]

Johan Commelin said:

Does docs/undergrad.yaml help a bit?

I am also curious about how to extract a subset of mathlib4 and create a mini-mathlib that specifically focuses on a small math domain such as elementary number theory or ring algebra, for example. It is challenging for me to handle and learn such a vast array of mathematical topics.

Could you please advise me on how to accomplish this? I would like to have a more focused and manageable version of mathlib4 that aligns with my specific interests.

If, for example, I want to focus solely on number theory, what is the minimum subset of mathlib4 that I should include to cover this topic? I assume that I should include the Mathlib/NumberTheory directory, select files from the Mathlib/Data directory, as well as relevant files from the Mathlib/Tactic directory, among others.

[Kevin Buzzard]

Take a look at the sections in the course I'm teaching now https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

[Chris Wong]

Johan Commelin said:

Chris Wong please add such things to https://leanprover-community.github.io/mathlib-overview.html

The undergrad.yaml is quite strictly aligned with the French undergrad curriculum (see note at the top of the page). And I think there is some value in that, because it provides an "external benchmark".

Thanks. I did see the note but I don't speak French :laughing:

Google Translate tells me those topics are listed at the bottom, as part of one of four electives. I guess the undergrad list focuses on the mandatory topics only.

[Jon Eugster]

Shaonan Wu said:

If, for example, I want to focus solely on number theory, what is the minimum subset of mathlib4 that I should include to cover this topic? I assume that I should include the Mathlib/NumberTheory directory, select files from the Mathlib/Data directory, as well as relevant files from the Mathlib/Tactic directory, among others.

The import-graph tool might help you at least somewhat getting an inside in the structure of mathlib: With the command

lake exe graph --to Mathlib.NumberTheory.Basic --exclude-meta --reduce number_theory.pdf

you can create a PDF showing all files imported by the file Mathlib.NumberTheory.Basic.
number_theory.pdf

[Shaonan Wu]

Jon Eugster said:

Shaonan Wu said:

If, for example, I want to focus solely on number theory, what is the minimum subset of mathlib4 that I should include to cover this topic? I assume that I should include the Mathlib/NumberTheory directory, select files from the Mathlib/Data directory, as well as relevant files from the Mathlib/Tactic directory, among others.

The import-graph tool might help you at least somewhat getting an inside in the structure of mathlib: With the command

lake exe graph --to Mathlib.NumberTheory.Basic --exclude-meta --reduce number_theory.pdf

you can create a PDF showing all files imported by the file Mathlib.NumberTheory.Basic.
number_theory.pdf

Thank you, I will try it.

[Shaonan Wu]

Perhaps we can create a simple mini mathlib4 designed for high-school or undergraduate-level math. This library will be accessible to students at that level and will assist them in learning how to use Lean from an early stage. :smiley:

[Luigi Massacci]

I think teaching high school math with Lean is bound to be as successful as the New Math movement of the 60's, which is to say not very successful at all.

Secondary school pedagogy aside, I think your plan is counterproductive even on principle: assuming for the sake of argument you could manage to get a subset of mathlib to work, it would still be:
a) Huge. Just look at the monstrous dependency tree @Jon Eugster made for you.
b) Wouldn't solve the "eccessive generality" problem you have encountered. The simple lemmas about integers you might be looking for will still be stated abstractly as properties of UFDs & co.

... so you are back where you began. What you really want is something like what is discussed here, #mathlib4 > Project idea: linking MathLib to math books, for some "Intro to Number Theory" textbook, which will presumably happen eventually. Then you won't care if the theorem technically has an hypothesis like [IsPrincipalIdealRing R] that you might not be familiar with, you'll just put ℤ as suggested in the tagged textbook and trust in typeclass inference.

[Shaonan Wu]

Luigi Massacci said:

I think teaching high school math with Lean is bound to be as successful as the New Math movement of the 60's, which is to say not very successful at all.

Secondary school pedagogy aside, I think your plan is counterproductive even on principle: assuming for the sake of argument you could manage to get a subset of mathlib to work, it would still be:
a) Huge. Just look at the monstrous dependency tree Jon Eugster made for you.
b) Wouldn't solve the "eccessive generality" problem you have encountered. The simple lemmas about integers you might be looking for will still be stated abstractly as properties of UFDs & co.

... so you are back where you began. What you really want is something like what is discussed here, #mathlib4 > Project idea: linking MathLib to math books, for some "Intro to Number Theory" textbook, which will presumably happen eventually. Then you won't care if the theorem technically has an hypothesis like [IsPrincipalIdealRing R] that you might not be familiar with, you'll just put ℤ as suggested in the tagged textbook and trust in typeclass inference.

Thank you for your valuable opinion. I understand that extracting a mini-mathlib4 is indeed challenging for me. As a student majoring in AI, my original intention in extracting a small subset of mathlib4 is to conduct AI research within a specific and well-defined mathematical domain. Especially I believe it is really hard for an AI theorem prover to perform effectively across all math domains.

[Patrick Massot]

The other solution is to restart from scratch and have an elementary library but this is a lot of work.

[Shaonan Wu]

I have one more question here. Since the dependencies of a single Mathlib file are so complex, so how to avoid the namespace pollution or conflicts.

[Kim Morrison]

Could you explain what you mean in more detail? I don't understand your question.

[Shaonan Wu]

Scott Morrison said:

Could you explain what you mean in more detail? I don't understand your question.

Sorry for my bad English.
I mean when you import a module in Lean, all the modules that it imports are also included in the context of your current Lean file. Dependencies are transitively included so that you have access to all the necessary definitions, theorems, and lemmas that the imported module relies on.

At the same time how to avoid namespace pollution or conflicts?

[Shaonan Wu]

When attempting to prove something in Lean, is there a guideline or recommendation on the minimal set of modules that should be imported? I'm curious about the smallest module set that would provide the necessary tools for the proof.

[Yaël Dillies]

You can type #minimize_imports after a proof to see what imports it uses