Starting out with Lean

Stream: new members

[Leo Shine]

Hi,

I'm interested in learning about how to use lean for formalising mathematics, but I'm not really sure where I'd want to go next after getting through various tutorials, seems like it would be really easy to try to formalize and prove something that turns out to be difficult and frustrating just because I chose a bad thing to try to start with, for some weird technical reason that I don't understand yet.

[Horatiu Cheval]

If you've already went through the tutorials then I think it's probably best to try to formalize some mathematics just for fun, and don't worry if you don't get it right the first time. It's surely possible and even probable that you will fall in various pitfalls at the start, but you can't really learn to avoid all of them until you really start formalizing things :)

[Horatiu Cheval]

It might be advisable to formalize something you are already mathematically comfortable with, and to not try to learn both some new math and lean at the same time

[Alex J. Best]

Feel free to ask about a few specific topics that interest you here, people will be more than happy to give advice. In general picking something that's no too far from things already in mathlib is good, so that you don't have too much groundwork to do yourself. As Kevin always says, proving theorems is generally easier than making good definitions as a newcomer. So proving something new about (a special type of) object already in mathlib is a great way to start I think.

[Leo Shine]

Sounds good,

Going to try to prove the statement that absolutely convergent series have the same sum after rearranging the elements in it

[Kevin Buzzard]

We don't have the definition of the sum of a non-absolutely-convergent sequence I don't think

[Kevin Buzzard]

I think convergence is defined in general as limit over the "tends to infinity" filter on the finite subsets of the index type

[Kevin Buzzard]

Convergence for this filter for a series of reals is a stronger than the regular notion of convergence which we teach to undergraduates -- it's equivalent to absolute convergence in fact

[Kevin Buzzard]

In fact probably a nice lean proof of this would be to define absolute convergence, prove it's equivalent to convergence for the filter we use to sum, and then use the fact that an equiv between types pulls back this "tends to a limit along all finite sets" filter pulls back to itself

[Anatole Dedecker]

I think Kevin is talking about docs#summable here, which is built to make rearrangement possible. Then, we already know that, in a finite-dimensional normed space over the reals, a family is summable iff the family of norms is summable two (see docs#summable_norm_iff). And then you could use docs#has_sum_iff_tendsto_nat_of_nonneg to conclude.

[Anatole Dedecker]

But if you want to prove it from scratch using epsilons and deltas it's a good exercise anyway of course