Learning materials on calculus in Lean

Stream: new members

[Kalle Kytölä]

Hi! I was asked: What are good learning materials on differential calculus in Lean? I realized I don't have a great answer, so I'm forwarding the question here in case others have good suggestions.

The general answer is probably the Learning resources page anyway.

More specifically geared towards calculus, the following ones came to my mind:

• #mil, i.e., Mathematics in Lean (Chapter 9 is specifically on differential calculus and Chapter 10 on integration)
• Lean for the Curious Mathematician 2023, probably particularly Oliver Nash's tutorial on Analysis (I haven't yet watched it myself, though)
• Heather Macbeth's The mechanics of proof course seems very appropriate as a learning material for calculus style, although I guess it doesn't literally contain calculus.

Am I missing important ones or are there other helpful comments to take into account here?

[Patrick Massot]

I think you have everything. We can extend what is in #mil if you feel this isn't good enough as a starting point.

[Kalle Kytölä]

Thank you!

I now tried to check out the LFTCM2023 video tutorial on analysis by @Oliver Nash myself. But the link on the webpage seems to lead to the topology session rather than analysis session. Would any of the organizers be able to fix the link?

[Patrick Massot]

Sounds good to me.

[Kalle Kytölä]

I also wanted to encourage newcomers to search the docs for results. Unfortunately, I found the results with the following searches on a few key undergraduate topics rather disappointing --- perhaps the docs are not meant to be used by entering standard mathematical keywords? But I think a person starting to learn Lean might reasonably expect to find the following ones in the docs:

• Fundamental Theorem of Calculus
• Integration by Parts
• Rank Nullity Theorem
• Contraction Mapping Principle
• First Isomorphism Theorem for Groups
• Cauchy Integral Formula
• Diagonalizability of Hermitian Matrices (I changed to "Hermitian Matrix", as a presumably better search term)
• Binomial Formula
• Fatou's lemma

There was exactly 1 of those 9 that resulted in a reasonable hit in the docs. I remembered that in Mathlib3 the situation was not like that --- even in some demos I asked the audience to suggest results and searched the Mathlib3 docs and looked up the formalized result, to (try to) convince mathematicians that Lean syntax of the statements is not unreadable (the syntax palatability aspect went down less well than I had imagined). I definitely remember finding the results.

I then made a small (not very scientific) comparison, and noticed that Mathlib3 docs indeed have reasonable hits for 5 out of the 9:

[Kalle Kytölä]

Search terms and results in online documentation of Mathlib3 and Mathlib4:

Fundamental Theorem of Calculus

(docs3) docs3#continuous_on.integral_sub_linear_is_o_ae :check:
(docs4) AlgebraicGeometry.instAlgebraCommRingFunctionFieldObj... :sad:

Integration by Parts

(docs3) (no results) :sad:
(docs4) FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebra... :sad:

Rank Nullity Theorem

(docs3) docs3#rank_range_add_rank_ker :check:
(docs4) instLieGroupRealToNontriviallyNormedFieldDensely... :sad:

Contraction Mapping Principle

(docs3) (no results) :sad:
(docs4) AlgebraicGeometry.StructureSheaf.instAlgebraCommRingStalkComm... :sad:

First Isomorphism Theorem for Groups

(docs3) (no results) :sad:
(docs4) BoundedContinuousFunction.instStarModuleBoundedContinuousFunctionToPseudo... :sad:

Cauchy Integral Formula

(docs3) docs3#complex.cderiv :looking: - 2nd hit is docs3#complex.circle_integral_div_sub_of_differentiable_on_off_countable :check:
(docs4) PresheafOfModules.instAdditivePresheafOfModulesFunctorOppositeOppositeAdd... :sad:

Hermitian Matrix (Diagonalizable)

(docs3) docs3#matrix.is_hermitian.eigenvector_basis :check:
(docs4) docs#Matrix.IsHermitian.eigenvectorMatrix :check:

Binomial Formula

(docs3) (no results) :sad:
(docs4) BilinForm.instIsCentralScalarBilinFormInstSMulBilinFormMulOppositeMonoidOp... :sad:

Fatou's lemma

(docs3) docs3#measure_theory.lintegral_liminf_le' :check:
(docs4) adicCompletion.instIsHausdorffSubtypeForAllNatQuotientSubmodule... :sad:

[Kalle Kytölä]

Could it be that in Mathlib4 documentation searches, the docstring of the theorem is not searched? Given that the docstrings contain the closest equivalent to ordinary mathematics, I would hope that especially those are included in the search.

Searching for docstrings would also be a way to include only reasonable theorems rather than the uninteresting lemmas. It was even proposed that the difference between a lemma and a theorem is that a linter requires a docstring for the latter.

[Jireh Loreaux]

Yes, at some point in mathlib3 we started searching docstrings, but I don't think that has made it to doc-gen4 yet, @Henrik Böving ?

[Henrik Böving]

Hm, I was thinking people would use loogle for doc string search maybe?

[Henrik Böving]

Because I dont have the doc string search on purpose as they are actually a couple of MB long by now so they slow down search and load time noticeably

[Kalle Kytölä]

I think it makes a big difference in real-life search queries.

[Jireh Loreaux]

Does loogle even search docstrings? Also, loogle I think needs at least one expression, it can't search only declaration names.

[Kalle Kytölä]

My oversimplified mental picture was:

• loogle if you already know the relevant Lean terms
• documentation search if you know the math term.

The latter seems far more relevant to newcomers.

[Joachim Breitner]

Loogle doesn’t search through docstrings; not sure if it should, as Kalle says that’s a somewhat different usecase.

[Mario Carneiro]

it should definitely be able to search docs

[Mario Carneiro]

I suspect you should just do that by default for "text" queries

[Henrik Böving]

Kalle Kytölä said:

My oversimplified mental picture was:

• loogle if you already know the relevant Lean terms
• documentation search if you know the math term.

The latter seems far more relevant to newcomers.

Well my idea eventually was to maybe have a page like docs.rs and then not use the doc-gen search at all but instead a loogle one integrated into doc-gen? And only still provide doc-gen search as a fallback for local documentation or something like that

[Kevin Buzzard]

My model of doc search can be used for two different things: looking for a term, and looking for a string. I use doc search to to both. In lean 3 there were two different ways to search docs -- you could type in the box and then click on the term in the drop down list, or you could type in the box and click on Google site search, which worked for strings.