Zulip Chat Archive

Stream: new members

Topic: Hi!


view this post on Zulip 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!

view this post on Zulip Johan Commelin (Jun 11 2019 at 14:47):

Welcome!

view this post on Zulip Johan Commelin (Jun 11 2019 at 14:47):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 11 2019 at 14:49):

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

view this post on Zulip Johan Commelin (Jun 11 2019 at 14:49):

So the library is very skewed.

view this post on Zulip 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.?

view this post on Zulip Kenny Lau (Jun 11 2019 at 14:58):

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

view this post on Zulip Kenny Lau (Jun 11 2019 at 14:58):

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

view this post on Zulip Chun Hong Lo (Jun 11 2019 at 15:14):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 16:59):

Are you in the maths department there?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 16:59):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 11 2019 at 21:48):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:49):

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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 11 2019 at 21:52):

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

view this post on Zulip Reid Barton (Jun 11 2019 at 21:52):

And the student gets to make the number go up

view this post on Zulip Mario Carneiro (Jun 11 2019 at 22:09):

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

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 12 2019 at 15:01):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 12 2019 at 18:40):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 19:35):

I think @Patrick Massot has a pretty good idea

view this post on Zulip 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