Hi!

Stream: new members

[Chun Hong Lo]

Hi all!

I'm a graduate student at MIT. I'm new to Lean, but I've been interested in learn about Lean (and might actually get onto it now that it's summer). Anyway, I have a few talented high school students (i.e. comfortable with a good chunk of undergraduate math) and they've been looking for stuff to do over the summer. It seems to me that this might be an appropriate place for them to find something to contribute to - but I'm a bit unfamiliar as to what's already done / being worked on etc. I would really appreciate it if someone could give me some pointers.

Thanks!

[Johan Commelin]

Welcome!

[Johan Commelin]

Most of us mathematicians are struggling quite hard to formalise basic things (-;

[Johan Commelin]

I'm not exactly sure what kind of contributions you are thinking of... mathematical things or more recreational things?

[Johan Commelin]

To give you an idea: at the moment it is a gigantic task to show that the derivative of exp is exp. And indeed, this task has not been done yet.

[Johan Commelin]

On the other hand, we have some pretty advance commutative algebra done

[Johan Commelin]

So the library is very skewed.

[Chun Hong Lo]

To be honest I'm not sure what kind of contributions I'm thinking of either. Is there a place where I can see something like 'ongoing tasks' / 'what we have so far' etc.?

[Kenny Lau]

https://github.com/leanprover-community/mathlib/pulls?page=1&q=is%3Apr+is%3Aopen

[Kenny Lau]

https://github.com/leanprover-community/mathlib/commits/master

[Chun Hong Lo]

This seems like what I've been looking for. Thanks!

[Kevin Buzzard]

Are you in the maths department there?

[Kevin Buzzard]

@Kenny Lau will be at MIT next semester; he's a big contributor to mathlib.

[Chun Hong Lo]

Yeah! I've talked to Kenny - in fact he recommended me to show up in this chat

[Kevin Buzzard]

To give you an idea: at the moment it is a gigantic task to show that the derivative of exp is exp. And indeed, this task has not been done yet.

Is it really a gigantic task? This is just a question of showing a power series can be differentiated term by term within its radius of convergence. I guess we're still waiting for the differentiation API but gigantic? Isn't it just a bit tedious and long?

[Reid Barton]

Very recently there's been a bit of interest here in the 100 theorems list. A lot of easy items on the list haven't been done, and there's quite a range of potential projects.

[Reid Barton]

For example proving that the harmonic series diverges might be a good first project.

[Kevin Buzzard]

@Chun Hong Lo that would make a very interesting project. For many of the theorems on the list, people here would know in theory how to do it, it's just finding the time.

[Kevin Buzzard]

Many people here have got their own projects that they're working on.

[Reid Barton]

(Also see https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md, http://bim.shef.ac.uk/lean/hundred_theorems.html.)

[Reid Barton]

One issue is that many of these are kind of useless from a math library perspective, but for a first project that's not necessarily such a bad thing

[Kevin Buzzard]

In fact I know from experience that many first projects by beginners are in no shape at all to go into a maths library.

[Reid Barton]

So we can just point to it and say someone did it, and that's fine

[Reid Barton]

And the student gets to make the number go up

[Mario Carneiro]

The theorems are mostly useless but the library building needed to prove the theorems are not

[Chun Hong Lo]

Thanks for all the references -- it makes sense that first projects by beginners are unlikely to be appropriate for the maths library but that's absolutely fine. I'll probably be back with more concrete questions later, once I learn some of the basics first :)

[Scott Morrison]

There's also the issues list, https://github.com/leanprover-community/mathlib/issues, which I'd love to see become a clearing house for good problems for newcomers to work on.

[Kevin Buzzard]

I have some random mathematical issues which I still didn't add to the issues page, but the problem is that all of them will involve creating some new structures, and there is an art to this which a beginner probably will not have.

[Johan Commelin]

Ok, maybe gigantic was a bit of an exaggeration. But it is definitely a lot more work than a mathematician would naively expect it to be.

[Yao Liu]

Hi all, I'm new too, and my uninformed opinion is that analysis is much harder to formalize than algebra, topology, category theory... because of the many different definitions one could make about such simple objects as exp. As someone remarked on MathOverflow, exp has three natural definitions: power series, inverse to log=\int dx/x, and lim(1+x/n)^n. If we want to prove a specific fact about exp, we could choose the easiest definition for that purpose; but for a formalization project, we'd need to have all three, and prove their equivalence. It's further complicated by the fact exp is also a complex-analytic object.

Same goes with (constructions of) real numbers.

[Johan Commelin]

I know of 3 different definitions of the p-adic integers...

[Reid Barton]

The good thing is that all the different definitions of exp are actually equal (and not just isomorphic)

[Reid Barton]

I think one thing that is perhaps holding up analysis is that maybe we don't know (at least I certainly don't know) what the optimum level of generality is. For example it wouldn't be hard to prove the theorems from a real analysis course on convergent series, but it's clearly not the right level of generality.

[Reid Barton]

But I never learned enough analysis to know what the correct level of generality is

[Kevin Buzzard]

Johannes made multivariate polynomials but it became clear quickly that we still needed single-variable ones so Chris made them too.

[Chris Hughes]

I think I did them wrong though. All the structure should have come from mv_polynomial first to shorten the theory

[Yao Liu]

Exactly. An obvious first goal would be the fundamental theorem of calculus, and there already are multiple issues with the level of generality, the least of which being: Are functions real-valued or complex-valued (if you have Cauchy's integral formula in mind), or as Bourbaki would have it, taking values in a topological vector space? I always felt this was excessive, but when I did sit down and try to write it down, that's what I ended up too...

Do remember that Bourbaki (or Weil in particular) started out trying to write a text for analysis, which finally came after volumes of algebra and topology—though it was only "functions of a single real variable" and doesn't seem to have much on convergence of series, if I recall. It's probably at the "optimum level of generality" as it gets, being Bourbaki after all.

Not totally unrelated, there is a rumor that Bourbaki was working on a volume on differentiable manifolds, and Grothendieck wanted to base it on sheaves and categories... they ended up with only a "summary of results" on manifolds. We all wonder what it would have been like if Grothendieck had his way.

[Kevin Buzzard]

I think @Patrick Massot has a pretty good idea

[Sebastien Gouezel]

Analytic functions in several variables are done in proper generality for instance in Mujica, complex analysis in Banach spaces (see the first chapter there). But this will be so much more complicated than one single variable that I think it is definitely worth it to do a separate theory in one variable (first, and probably keep it forever). Complex analysis in one variables also has several features that simply do not exist in several variables.

[Alex Zorn]

Hey all, my name is Alex Zorn! I have a math PhD from Berkeley, but have since left academia. Currently located in nyc. Interested in learning more about lean and hoping to maybe get to the point where I can contribute something useful. How is everyone doing tonight?

[Alex Zorn]

Also- the guide says I should ask for write access to non-master branches of the mathlib repository. Username on github is "Alex-Zorn"

[Kevin Buzzard]

What kind of things were you thinking of contributing? Maybe this could wait until you're ready to contribute?

[Alex Zorn]

Sure. My main interests would maybe be something in representation theory (do we have, like, classification of reps of semisimple Lie algebras?), or statistics (according to the site we don’t have a proof of CLT). But happy to join in any project that could use a hand.

[Richard Osborn]

The classification of semisimple Lie algebras is currently being worked on. You can track the project here. I'm sure they'd welcome any additional help.

[Josha Dekker]

@Rémy Degenne is working on CLT!

[Rémy Degenne]

I am not really working on it, no. Some people expressed interest in formalizing CLT some time ago, so I started a project (https://github.com/RemyDegenne/CLT, https://remydegenne.github.io/CLT/, not very polished) to help guide the formalization. But the interest apparently melted instantly and nothing happened (not blaming anyone, that happens with projects where people freely contribute when they have time and feel like it). And since I have several other projects I prefer working on, I am not spending time alone on that one.

If you want to formalize the central limit theorem yourself, do it! It's an good project idea. Don't feel blocked by the fact that others might also have some partial work towards it. I am definitely not "claiming" CLT for myself or my project.

[Josha Dekker]

Yes, I was one of them but got stuck by my inadequacy at properly handling integrals in Mathlib… I’ve been meaning to return to work on CLT, but I haven’t found the time yet!

[Alex Zorn]

@Richard Osborn thanks! What’s the best way for me to introduce myself to the people working on that? Is there a thread in Zulip or something?

[Jireh Loreaux]

Almost certainly you'll want to talk to Oliver Nash. He's not subscribed to this stream, so you'll need to contact him directly, or post a thread in a different stream and @ mention him there.

[Josha Dekker]

Rémy Degenne said:

I am not really working on it, no. Some people expressed interest in formalizing CLT some time ago, so I started a project (https://github.com/RemyDegenne/CLT, https://remydegenne.github.io/CLT/, not very polished) to help guide the formalization. But the interest apparently melted instantly and nothing happened (not blaming anyone, that happens with projects where people freely contribute when they have time and feel like it). And since I have several other projects I prefer working on, I am not spending time alone on that one.

If you want to formalize the central limit theorem yourself, do it! It's an good project idea. Don't feel blocked by the fact that others might also have some partial work towards it. I am definitely not "claiming" CLT for myself or my project.

@Rémy Degenne I see that you have a definition for tight measures in there, are you developing that specific theory more in another repo, or is that currently standing still? If the latter, I'd be happy to try and code up some basic API for tight measures and PR it directly to Mathlib, if you like/don't mind! Let me know!

[Rémy Degenne]

I am not working on it. If you have time to develop tight measures and add them to mathlib, that would be great. You can take anything you want from that repository.

[Josha Dekker]

Rémy Degenne said:

I am not working on it. If you have time to develop tight measures and add them to mathlib, that would be great. You can take anything you want from that repository.

great, thanks! I've been meaning to work on more probability-theory related stuff, and just realised that this might be a good next project for me! I'll check in a new post if nobody else is working on this!

[Kevin Buzzard]

I think that having interesting conversations under a thread called "Hi!" will make them harder to find later on, so I'm very glad you're moving to a new post!

[Timo Carlin-Burns]

@Alex Zorn welcome! There are a few more Lean enthusiasts in NYC and we've been talking about meeting up. You would be welcome to join! Here is the thread if you're interested https://leanprover.zulipchat.com/#narrow/stream/224796-Geographic-locality/topic/New.20York.20City.2C.20USA/near/435689728