Project suggestions

Stream: LftCM22

[Heather Macbeth]

ICERM_projects.pdf

[Elif Sacikara (Alumni)]

how much background (both on the proposed math notions and lean implementation) should we have to join a project (if it is open to online participants as well)?

[Jireh Loreaux]

https://leanprover.zulipchat.com

[Ryan McCorvie]

I'm game to try C^k version of existence / uniqueness of ODEs. Or power series identities.

[Flo]

Question about the general outcome of a given project:

If one proves Fubini’s theorem in Lean, for instance, will it/should it be immediately possible to use it to compute Gaussian integrals? Or is the “distance” between a theorem and its applications usually bigger in Lean?

[Jackie Lang]

I have almost no Lean experience, but I would be interested in being in touch with any people working on the quadratic fields project.

[Alba Marina MÁLAGA SABOGAL]

Same here, basically a newbie in LEAN, but if there are people enthousiastic with the length space project and the proof of hyperbolic plane being a length space, I am interested in following along.

[Flo]

From the suggestion given during Heather's talk, I like the one about H-spaces! I would also be interested in getting in touch with people interested in basic complex variable theory (Cauchy's theorem, residue formula, etc.).

I also have very little experience for now.

[Heather Macbeth]

Flo said:

Question about the general outcome of a given project:

If one proves Fubini’s theorem in Lean, for instance, will it/should it be immediately possible to use it to compute Gaussian integrals? Or is the “distance” between a theorem and its applications usually bigger in Lean?

Hi @Flo ! Fubini's theorem is already in Lean in fact. So you could try the Gaussian integrals step.

[Heather Macbeth]

You can message @Yury G. Kudryashov about complex analysis and @Filippo A. E. Nuccio about H-spaces.

[Sahana Balasubramanya]

I am also new to Lean. But based on my research/lean experience, either the length spaces project or the power series project would be of interest to me.

[Heather Macbeth]

Elif Sacikara (Alumni) said:

how much background (both on the proposed math notions and lean implementation) should we have to join a project (if it is open to online participants as well)?

Hi @Elif Sacikara (Alumni) ! Feel free to join a project if you can consult on the mathematics, even if not hte Lean yet.

[Anatole Dedecker]

Flo said:

Question about the general outcome of a given project:

If one proves Fubini’s theorem in Lean, for instance, will it/should it be immediately possible to use it to compute Gaussian integrals? Or is the “distance” between a theorem and its applications usually bigger in Lean?

In general, relatively to the math difficulty, computations tend to be harder to formalize than abstract stuff imo. But the aim is definitely to make enough API to make theorems usable in practice

[Filippo A. E. Nuccio]

Flo said:

From the suggestion given during Heather's talk, I like the one about H-spaces! I would also be interested in getting in touch with people interested in basic complex variable theory (Cauchy's theorem, residue formula, etc.).

I also have very little experience for now.

Hi @Flo : I am happy to work about H-spaces, are you here in Providence?

[Yury G. Kudryashov]

I'm ready to answer questions about complex analysis

[Yury G. Kudryashov]

Here or in person

[Flo]

Thanks Heather Macbeth ! Yes, I will try the Gaussian integrals step, that will be good practice for me. Then I will contact Yury and/or Filippo.

[Johan Commelin]

@Jackie Lang I pinged @Kevin Buzzard about the quadratic field project

[Filippo A. E. Nuccio]

I am here when you want.

[Flo]

Anatole Dedecker said:

Flo said:

Question about the general outcome of a given project:

If one proves Fubini’s theorem in Lean, for instance, will it/should it be immediately possible to use it to compute Gaussian integrals? Or is the “distance” between a theorem and its applications usually bigger in Lean?

In general, relatively to the math difficulty, computations tend to be harder to formalize than abstract stuff imo. But the aim is definitely to make enough API to make theorems usable in practice

I see! Good to know! Thanks :-)

[Heather Macbeth]

Hi @Alba Marina MÁLAGA SABOGAL and @Sahana Balasubramanya , a couple of in-person participants are also interested in length spaces: @antonio montalban and @Sam Freedman . I'll connect you after they join Zulip.

[Heather Macbeth]

Sahana, @Emil Sköldberg was also interested in power series, if you'd rather work on that.

[Sahana Balasubramanya]

@Heather Macbeth : That sounds great ! Thanks !

[Alba Marina MÁLAGA SABOGAL]

Heather Macbeth said:

Hi Alba Marina MÁLAGA SABOGAL and Sahana Balasubramanya , a couple of in-person participants are also interested in length spaces: Antonio Montalban and Sam Freedman . I'll connect you after they join Zulip.

Thanks,

[Kevin Buzzard]

Jackie Lang said:

I have almost no Lean experience, but I would be interested in being in touch with any people working on the quadratic fields project.

@Jackie Lang hi! I'm talking to Daniel Hast from BU in person. @Daniel Hast oh there you are :-) Maybe let's move elsewhere? Hang on

[Flo]

@Filippo A. E. Nuccio @Yury G. Kudryashov I am in France right now, so everything would have to be online.

H-spaces seem to form a directly accessible, clear-cut project, which is nice.

And in the middle to long run, I am interested in contributing to complex analysis, which is a subject I have taught in the past and is close to my research area (things about Riemann surfaces).

[Flo]

@Yury G. Kudryashov Is Cauchy formula already in mathlib? I found this: theorem sum_cauchy_power_series_eq_integral. I guess I should start by knowing precisely what is already available!

[Elif Sacikara (Alumni)]

Heather Macbeth said:

Elif Sacikara (Alumni) said:

how much background (both on the proposed math notions and lean implementation) should we have to join a project (if it is open to online participants as well)?

Hi Elif Sacikara (Alumni) ! Feel free to join a project if you can consult on the mathematics, even if not hte Lean yet.

Thank you @Heather Macbeth! Well, I think I will be happy to part of the Galois Group of x^n-a (Kummer Theory).

[Yury G. Kudryashov]

We have Cauchy integral formula for some domains

[Yury G. Kudryashov]

See docs#differentiable_on.has_fpower_series_on_ball

[Yury G. Kudryashov]

Better: docs#diff_cont_on_cl.circle_integral_sub_inv_smul

[Tyler Raven Billingsley]

I looked at the elliptic curve part of mathlib and was surprised to see very little there. Would it be reasonable to try to pursue formalizing the basics of elliptic curves over fields (i.e. the classical setting as in Silverman's AEC)? Is it essential to build things up for general rings first? Are there significant obstructions that the experts have thought through?

[Mario Carneiro]

The general recommendation is that even if you want to do it over fields, you should write each theorem and definition with the weakest assumptions for which it still typechecks

[Mario Carneiro]

that does not mean you have to actually properly engage with what an elliptic curve over a semiring should mean - if a theorem of interest isn't true in that generality then just add more hypotheses to bring it back to sanity

[Mario Carneiro]

(but working out what these things actually do mean in weirdly general settings is a popular pastime when doing this kind of formalization, because the question, once asked, begs for an answer)

[Kevin Buzzard]

@Tyler Raven Billingsley my student @David Ang has been working on Mordell-Weil!

[Kevin Buzzard]

I would happily try and lead a project on etale cohomology. I think the starting point is etale morphisms of rings. I think that this project should be relatively straightforward if a student who knew or wanted to learn the theory of etale morphisms of rings explained e.g. I think in Freitag-Kiehl. Apparently I'm giving a talk on algebraic geometry on Friday so I could just talk about that if we got anywhere.

My student Amelia Livingston (who doesn't use Zulip much) has been doing group and Galois cohomology (Sebastian Monnet made the Krull topology on an infinite Galois group) so etale cohomology is a very nice next step and it's probably in scope.

[Kevin Buzzard]

After making a robust API for etale morphisms of rings the challenge would be to globalize it so that you can get a definition of an etale morphism of schemes.

[Kevin Buzzard]

@Judith Ludwig @Jackie Lang I know this rounds ridiculous but this would be much easier than discriminants of quadratic fields

[Flo (Florent Schaffhauser)]

Hi! Is there a Zulip stream for the covering spaces project? I can't seem to find it and I would be interested in participating or at least knowing about it :sweat_smile:

[Junyan Xu]

There is a topic in an obscure stream ...

[Thomas Browning]

The pull request #15276 contains the current definition of covering spaces. The next (hard!) thing is to prove homotopy lifting. But proving other basic properties would be appreciated.