# Zulip Chat Archive

## Stream: new members

### Topic: Hi!

#### Chun Hong Lo (Jun 11 2019 at 14:44):

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 (Jun 11 2019 at 14:47):

Welcome!

#### Johan Commelin (Jun 11 2019 at 14:47):

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

#### Johan Commelin (Jun 11 2019 at 14:48):

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

#### Johan Commelin (Jun 11 2019 at 14:49):

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 (Jun 11 2019 at 14:49):

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

#### Johan Commelin (Jun 11 2019 at 14:49):

So the library is very skewed.

#### Chun Hong Lo (Jun 11 2019 at 14:57):

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 (Jun 11 2019 at 14:58):

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

#### Kenny Lau (Jun 11 2019 at 14:58):

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

#### Chun Hong Lo (Jun 11 2019 at 15:14):

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

#### Kevin Buzzard (Jun 11 2019 at 16:59):

Are you in the maths department there?

#### Kevin Buzzard (Jun 11 2019 at 16:59):

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

#### Chun Hong Lo (Jun 11 2019 at 21:44):

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

#### Kevin Buzzard (Jun 11 2019 at 21:47):

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 (Jun 11 2019 at 21:48):

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 (Jun 11 2019 at 21:48):

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

#### Kevin Buzzard (Jun 11 2019 at 21:48):

@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 (Jun 11 2019 at 21:49):

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

#### Reid Barton (Jun 11 2019 at 21:49):

(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 (Jun 11 2019 at 21:51):

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 (Jun 11 2019 at 21:51):

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 (Jun 11 2019 at 21:52):

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

#### Reid Barton (Jun 11 2019 at 21:52):

And the student gets to make the number go up

#### Mario Carneiro (Jun 11 2019 at 22:09):

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

#### Chun Hong Lo (Jun 11 2019 at 22:31):

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 (Jun 11 2019 at 22:36):

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 (Jun 11 2019 at 22:46):

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 (Jun 12 2019 at 04:50):

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 (Jun 12 2019 at 14:56):

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 (Jun 12 2019 at 15:01):

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

#### Reid Barton (Jun 12 2019 at 16:41):

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

#### Reid Barton (Jun 12 2019 at 18:40):

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 (Jun 12 2019 at 18:40):

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

#### Kevin Buzzard (Jun 12 2019 at 18:42):

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

#### Chris Hughes (Jun 12 2019 at 18:43):

I think I did them wrong though. All the structure should have come from `mv_polynomial`

first to shorten the theory

#### Yao Liu (Jun 12 2019 at 19:34):

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 (Jun 12 2019 at 19:35):

I think @Patrick Massot has a pretty good idea

#### Sebastien Gouezel (Jun 12 2019 at 20:18):

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.

Last updated: May 09 2021 at 20:11 UTC