Beginning to contribute

Stream: new members

[Giovanni Mascellani]

Hi, after lurking here for some time and doing tutorials, I'd like to see if I'm able to contribute something to mathlib. Back when I was in the academia I used to work on geometric analysis, with a strong focus on PDEs. So I'd be interested in contributing either in the direction of PDEs or of Riemannian manifolds. I guess that both of these are still far in the future, but is there some work being done already, and some meaningful way in which a newbie like me can try to do something?

[Kevin Buzzard]

Riemannian manifolds -- we are still only just beginning with the theory of linear algebra on vector bundles; I feel like we are on the cusp of being able to make this definition but I don't know if we're quite there, and it would definitely be a terrifying job for a beginner. PDEs we have essentially nothing and are probably in a good position to start thinking about these. Can you suggest a simple goal?

[Giovanni Mascellani]

Reading what's already in mathlib it would seem that the next goal would be to define Sobolev spaces, which doesn't appear to be that simple. Maybe it might be sensible to warm up by defining Sobolev spaces on intervals of R and start proving simple properties there?

[Giovanni Mascellani]

My feeling is that laying down the definitions, and in general the setting of a theory, is easily one of the hardest parts. But it's also where you have to start from! (though the option of scratching everything and throwing it into a bin is always available, and often quite instructive too)

[Kevin Buzzard]

The other issue is that we are in a transition period right now, moving from Lean 3 to Lean 4, which complicates matters. It might be easiest just to make a Lean 3 project which depends on mathlib and try developing the theory there.

[Patrick Massot]

Giovanni, it's great to read you want to contribute to PDEs in Lean. We really need people from this area. @Heather Macbeth probably has a lot of interesting things to say about what are good targets for you.

[Kevin Buzzard]

Another issue is that definitions are much harder for Lean beginners than proofs. I think that trying to define Sobolev spaces W^{1,p} and W^{2,p} for (arbitrary?) subsets of R and then try W^{k,p} after; this way will introduce you to concepts one by one rather than all at once. Run the definitions past Zulip and see if people make suggestions. Literally just proving that they're vector spaces will already be a good exercise.

[Tomas Skrivan]

Out of purely selfish reasons I have one topic that is quite close to your interests. I'm working on automatic differentiation support for Lean and if we hope to verify it at some point it needs definition of Convenient vector spaces. It is a class of infinite dimensional vector spaces that form Cartesian closed category and that is the main result that is necessary.

This amounts to formalizing the first chapter of The Convenient Setting of Global Analysis I think the crux is theorem 3.2 and 3.4 and the main result is 3.12 and 3.12

The necessary theory to start this is of locally convex spaces, Gateaux derivative and Riemann integral. Which I think are all in mathlib but not yet ported.

[Giovanni Mascellani]

Kevin Buzzard said:

Another issue is that definitions are much harder for Lean beginners than proofs. I think that trying to define Sobolev spaces W^{1,p} and W^{2,p} for (arbitrary?) subsets of R and then try W^{k,p} after; this way will introduce you to concepts one by one rather than all at once. Run the definitions past Zulip and see if people make suggestions. Literally just proving that they're vector spaces will already be a good exercise.

Sure, I'll begin with that and see what happens. Thanks!

[Moritz Doll]

Hi, just a remark on Sobolev spaces: Heather and I had a discussion about this last (northern hemisphere) summer and we both agreed that this is quite a difficult thing to get right. I would think that what ends up happening for open subsets of $\mathbb{R}^d$ is that we will define Triebel-Lizorkin and Besov spaces and all the 'easy' spaces are just reducible defs.
I wonder whether we have enough stuff already to prove some of the classical explicit solutions for Laplace, heat and wave equation. That might be fun.

[Moritz Doll]

(i.e., something along the lines of Section 2.3 in Evans)

[Moritz Doll]

One reason why we don't have any PDE things yet is that we still have to build the relevant distribution theory and this hinges on quite a lot of super abstract functional analysis (essentially formalizing lots of Bourbaki's Topological Vector Spaces). On the other side, we also don't have a lot about unbounded operators, so the Hilbert space theory of partial differential operators is also in the far future.

[Giovanni Mascellani]

Hi, thanks for your reply. Well, I realize that working on advanced stuff with a beginner might be less pleasant, but if along your roadmap you come across something that I might try to tackle I'm happy to try. I did some work with Besov spaces back in the days, it's not completely new stuff to me, but still I full acknowledge it's not an easy starting step.

In the meantime I'll try to think about classical solutions as you suggest.

[Giovanni Mascellani]

In the meantime, can I have write access to the mathlib repository? Though for the moment the only thing I have to submit is a small typo fix. My GitHub username is giomasce.

[Ruben Van de Velde]

Giovanni Mascellani said:

In the meantime, can I have write access to the mathlib repository? Though for the moment the only thing I have to submit is a small typo fix. My GitHub username is giomasce.

@maintainers

[Riccardo Brasca]

You should have an invitation.

[Riccardo Brasca]

Let me know if you are interested also in mathlib4

[Giovanni Mascellani]

@Riccardo Brasca Thanks. It seems that that specific typo is already fixed in mathlib4, but my hope is to eventually be able to contribute there too, so I wouldn't mind being invited there too.

[Riccardo Brasca]

Done. Buon lavoro!

[Giovanni Mascellani]

Grazie!

[Ryan McCorvie]

@Giovanni Mascellani I have a penchant for analysis and I've also been thinking about first projects for formalization, if you'd like to work together on the classical solutions. Perhaps a good template is along the lines of Evans' "Partial Differential Equations" part I?

[Heather Macbeth]

Moritz Doll said:

I wonder whether we have enough stuff already to prove some of the classical explicit solutions for Laplace, heat and wave equation. That might be fun.

I think this would be a good project, but one task before getting started would be a good theory for integrating on balls in $\mathbb{R}^n$ by considering them as $S^{n-1}\times (0, R]$. I'm not even quite sure how this would look, maybe one should carefully analyze the kinds of reasoning steps about them which occur in a standard development of the theory, and write those steps as lemmas.

@Sebastien Gouezel has proved the change-of-variables formula in a very general form, so the basic ingredients are available.

[Eric Wieser]

Just to check, these are euclidean_space round balls and not I -> real square balls?

[Ruben Van de Velde]

I do love the concept of square balls

[Giovanni Mascellani]

Ryan McCorvie said:

Giovanni Mascellani I have a penchant for analysis and I've also been thinking about first projects for formalization, if you'd like to work together on the classical solutions. Perhaps a good template is along the lines of Evans' "Partial Differential Equations" part I?

Yeah, I started playing with that. So far I feel the same confidence with Lean that my one-year-old daugther has with Italian. But she's doing a lot of progress, so there's hope for me too. I set out to prove section 2.1 (smooth solutions for the transport equation with constant coefficients), and maybe eventually I'll be able to write a definition for being a smooth solution of that equation.

I'm happy to work on that together, though keep in mind that I have a day job and two kids, so my schedule is going to be rather hectic.

[Moritz Doll]

Heather Macbeth said:

Moritz Doll said:

I wonder whether we have enough stuff already to prove some of the classical explicit solutions for Laplace, heat and wave equation. That might be fun.

I think this would be a good project, but one task before getting started would be a good theory for integrating on balls in $\mathbb{R}^n$ by considering them as $S^{n-1}\times (0, R]$. I'm not even quite sure how this would look, maybe one should carefully analyze the kinds of reasoning steps about them which occur in a standard development of the theory, and write those steps as lemmas.

Sebastien Gouezel has proved the change-of-variables formula in a very general form, so the basic ingredients are available.

We have docs#polar_coord so I would suspect that all the ingredients for the more general version are there.

[Moritz Doll]

It might not be the worst idea to do everything in 1d first and generalize later, then you also don't have to worry about integrating in polar coordinates and docs#fderiv nonsense.

[Heather Macbeth]

Moritz Doll said:

We have docs#polar_coord so I would suspect that all the ingredients for the more general version are there.

But polar co-ordinates are really different from spherical co-ordinates, since $S^1=\mathbb{R}/\mathbb{Z}$ and there is no similar trick for higher spheres ...