Differential equations recommendation

Stream: general

[Martin Dvořák]

I will soon need to work with differential equations. I have heard about a few Lean 4 libraries that formalize differential equations. I would like to start reading one of them, but I am clueless about the differences between them. Hence I would like to get a recommendation for which library is best for me. I have the following needs.

• I want a beginner-friendly library because I have never studied differential equations. I am willing to put a lot of time and effort into studying it, but I need it to be accessible for a person without a strong math background.
• I want a self-contained library because I want to learn about differential equations from the library alone. I don't want to end up having to read a textbook or wikipedia (or any other information source that uses any other than Lean notation) in order to make sense of it.
• I want to learn the theory rather than to develop practical skills in solving differential equations.

Based on my preferences, can you recommend which Lean 4 library for differential equations will be the best study material for me?

[Joris van Winden]

Are you mainly interested in ODEs or PDEs? For PDEs, it is often the case that the 'theory' mostly consists of tools and techniques which can be applied in a variety of different settings.

[Martin Dvořák]

I guess I should start with ODEs.

[Martin Dvořák]

I definitely prefer a library that will allow me to move to PDEs with as little changes in notation as possible.

[Kevin Buzzard]

The area is huge and you might need to specify exactly what you're interested in. It's a bit like me saying "I will soon need to work with programming languages and I've heard that there are several. I would like a recommendation for which programming language is best for me. I will give you no further information."

[Kevin Buzzard]

Differential equations are used by everyone from differential geometers to analysts to applied mathematicians to statisticians to physicists, chemists etc. These people are all using different techniques to think about vastly different questions all of which have some kind of a D operator.

[Kevin Buzzard]

Even the beginner differential equation course we teach in pure maths is different to the beginner course in applied maths which is different to the one in physics etc

[Martin Dvořák]

The problem is that I know so little that I don't even know what I don't know. So let me start simple. Is there at least one area of differential equations for which there is a self-contained Lean library I could study?

[Kevin Buzzard]

How come you know that you'll soon need to work with differential equations?

If you've never seen anything before then my instinct is that you should be steering well clear of lean at this point and just reading the basic texts which high schoolers read, things like how to solve linear ODEs and so on. My instinct is that lean will make things far more difficult than they need to be because everything is written in such huge generality.

Here is a concrete example. I wanted to be able to solve basic differential equations like d^2y/dx^2=-y in lean in 2017 because this is what we teach the first years. The solutions are linear combinations of sin and cos. So I was arguing in 2017 that we needed sin and cos and the proof that the derivative of sin was cos. But I was told in no uncertain terms that we did not want to set up the theory of one-variable calculus (which is where literally everyone starts learning about differential equations) because one-variable calculus is a special case of multivariable calculus which needs integration of functions taking values in topological vector spaces which needs theories of integration which I had never heard of in my life and I'm a professional mathematician who took all the undergraduate analysis courses on offer in Cambridge. And indeed this is what came to pass in mathlib. So I'm not even sure that I would understand how to solve that simple differential equation using mathlib (and I still don't know what the Bochner integral is), but I can certainly solve it on paper because I learnt how to when I was in high school.

[Martin Dvořák]

When I say "a beginner-friendly library" I imagine a repository that contains important corollaries explicitly and not just "the minimum that allows me to do everything somehow".

[Martin Dvořák]

What those "important corollaries" are, I don't know, because I don't know anything.

[Martin Dvořák]

Kevin Buzzard said:

My instinct is that lean will make things far more difficult than they need to be because everything is written in such huge generality.

My main point is that I want to learn differential equations through Lean notation, not necessarily through Mathlib conventions.

[Martin Dvořák]

Kevin Buzzard said:

I learnt how to when I was in high school.

Did you mean to imply that you already learnt solving differential equations in high school?

If it is the case, I am really impressed. When I was in high school, all I could do was to eat glue.

[Michael Rothgang]

Based on my preferences, can you recommend which Lean 4 library for differential equations

I'd be positively surprised if the collection of such libraries were non-empty. If you find one, please share it here (and let's discuss if the contents can be raised to mathlib-level and PRed)!

[Michael Rothgang]

To elaborate, I'm not aware of many self-contained Lean libraries on any topic at all. (I guess the NNG counts, perhaps the Real Analysis game also, and probably a few siblings. Your thesis tries to do that with some research-level mathematics. Is that an exception or are there other projects?)
Most formalisation projects I have seen do reference an external source.

[Martin Dvořák]

Michael Rothgang said:

To elaborate, I'm not aware of many self-contained Lean libraries on any topic at all.
(...)
Most formalisation projects I have seen do reference an external source.

Sorry for my vagueness. I didn't mean "self-contained" as "doesn't depend on Mathlib". I meant "self-contained" in the same sense that my Ph.D. thesis is self-contained.
https://madvorak.github.io/2026_Dvorak_Martin_Thesis_draft.pdf
See Section 3.1 for example.

[Martin Dvořák]

PS: I apologize I wasn't reading your message carefully enough. Indeed, we seem to agree on what we mean by "self-contained".

[Martin Dvořák]

TBH, I was hoping that one of the developers of one of the libraries would step in and advertise why their repository is worth reading, even if it wasn't perfect. Right now, I am as clueless as I was when I created this thread.

[Moritz Doll]

Martin Dvořák said:

I definitely prefer a library that will allow me to move to PDEs with as little changes in notation as possible.

Are you aware how much variety there is in the study of PDEs? Notation is very much the least of your problems.
Also I would not recommend learning differential equations through Lean, that sounds like a very bad idea (for basically the reason Kevin said).

[Dominic Steinitz]

I thought it pertinent to quote Iserles here:

The opening line of Anna Karenina, ‘All happy families resemble one another, but each unhappy family is unhappy in its own way’, is a useful metaphor for the computation of ordinary differential equations (ODEs) as compared with that of partial differential equations (PDEs). Ordinary differential equations are a happy family; perhaps they do not resemble each other but, at the very least, we can write them in a single overarching form y′ = f(t, y) and treat them by a relatively small compendium of computational techniques. (True, upon closer examination, even ODEs are not all the same: their classification into stiff and non-stiff is the most obvious example. How many happy families will survive the deconstructing attentions of a mathematician?)

Partial differential equations, however, are a huge and motley collection of problems, each unhappy in its own way. Most students of mathematics will be aware of the classification into elliptic, parabolic and hyperbolic equations, but this is only the first step in a long journey. As soon as nonlinear – or even quasilinear – PDEs are admitted for consideration, the subject is replete with an enormous number of different problems and each problem clamours for its own brand of numerics. No textbook can (or should) cover this enormous menagerie. Fortunately, however, it is possible to distil a small number of tools that allow for a well-informed numerical treatment of several important equations and form a sound basis for the understanding of the subject as a whole.

[Martin Dvořák]

Moritz Doll said:

Are you aware how much variety there is in the study of PDEs?

No, I don't. The only thing I know about PDEs is that they are extremely difficult.

[Martin Dvořák]

Moritz Doll said:

Also I would not recommend learning differential equations through Lean, that sounds like a very bad idea (for basically the reason Kevin said).

The dealbreaker for me is that the Lean syntax is the only math notation I like.

[Martin Dvořák]

I don't know anything about PDEs, but I know that other mathematical areas can be explained through Lean. So I hope it will be possible here as well.

Many people say that in places where a formal statement is hard to read, it should be replaced or complemented by an informal statement to ease the reading.

I disagree. Instead, I say that in places where a formal statement is hard to read, the Lean notation should be improved so that reading the code is as easy as reading its informal counterpart (for a person that knows both syntaxes). There is no good excuse for making Lean definitions and theorem statements unnecessarily hard to read.

[Johan Commelin]

That Iserles quote maybe also gives a hint as to why there is so little about PDEs in Lean atm.

[Michael Rothgang]

... besides the usual reason "nobody did it before" and analysis in mathlib being less developed than some algebraic areas. (There is work underway to define Sobolev spaces; this shows that we are still missing basic prerequisites. This area can be worked on now, but it needs more people interested in doing so.)

[Martin Dvořák]

There have been some workshops dedicated to formalizing differential equations in Lean, haven't they?

[Michael Rothgang]

There was one at SLMath last October. @Rémy Degenne and I went and taught Lean to the attendees. We met a few people doing Lean, had good conversations about good next targets, and left with a better understanding of that (and hopefully a small contribution to evangelising Lean), but no particular group project aiming for mathlib-level code.

[Michael Rothgang]

(The Sobolev space work was already planned before, so I'm not counting that.)