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.