## Stream: maths

### Topic: things to formalise

#### Edward Ayers (Aug 07 2018 at 17:08):

Dear all, I've dabbled with Lean about a year ago. I worked through _theorem proving with lean_ but I didn't go much beyond that. I would like to formalise some easy undergraduate maths just to get back in to it. Any recommendations? I was thinking of doing just some basic groups, ring theory or linear algebra. Last time I looked at Lean they didn't have a formalisation of the reals. Is that still the case? If the reals have been formalised then perhaps doing some simple real analysis. What active existing libraries should I look at for this kind of thing? I am aware of Xena and the official lean library repo.

#### Patrick Massot (Aug 07 2018 at 17:09):

https://github.com/leanprover/mathlib/

#### Patrick Massot (Aug 07 2018 at 17:09):

is the main place

#### Edward Ayers (Aug 07 2018 at 17:13):

thanks. I now realise I should have put this in #new members

#### Kevin Buzzard (Aug 07 2018 at 17:22):

I hear from my undergrads that they are one lemma shy of proving det(AB)=det(A)det(B)

#### Kevin Buzzard (Aug 07 2018 at 17:23):

There is still no definition of the derivative of a function so no chain rule or product rule

#### Kevin Buzzard (Aug 07 2018 at 17:24):

There is still no proof that a power series is continuous within its radius of convergence which is the main holdup for defining pi

#### Patrick Massot (Aug 07 2018 at 17:25):

The chain rule is waiting for the norms PR

#### Kevin Buzzard (Aug 07 2018 at 17:25):

What is the problem with the norms PR?

#### Patrick Massot (Aug 07 2018 at 17:30):

Mario and Johannes want to work on it

#### Patrick Massot (Aug 07 2018 at 17:30):

that's all I know

#### Edward Ayers (Aug 07 2018 at 19:47):

@Kevin Buzzard can you point me to the relevant files in mathlib for the power series proof please?

#### Johan Commelin (Aug 07 2018 at 19:49):

I don't think power series are in mathlib.

#### Johan Commelin (Aug 07 2018 at 19:49):

So most likely there is no particular file to point to.

#### Kevin Buzzard (Aug 07 2018 at 19:53):

Hmm. Did @Chris Hughes 's work on the exponential function get accepted yet?

#### Patrick Massot (Aug 07 2018 at 19:55):

no. I think it tries to become the most venerable PR in mathlib

#### Kevin Buzzard (Aug 07 2018 at 19:56):

We are really bad at basic analysis. When Patrick says that the chain rule will come after normed spaces, he means the correct general chain rule for functions $\mathbb{R}^a \to\mathbb{R}^b$ but there's some hold-up with normed spaces that I'm not clear about. Johan might be right -- there might not even be a basic theory of power series in mathlib, although Chris must have done something because I'm pretty sure he defined $x\mapsto e^x : \mathbb{C}\to\mathbb{C}$. There was some hold-up with that PR as well -- I think that Mario and Johannes had different opinions about it and for a while at least we were just stuck in an impasse.

#### Kevin Buzzard (Aug 07 2018 at 19:57):

Oh! Looking at the comments, it seems that people were concerned that the PR did not use enough filters :-)

#### Patrick Massot (Aug 07 2018 at 20:00):

Come on Kevin. I mean functions between normed spaces, not $\mathbb{R}^a \to\mathbb{R}^b$. And I don't mean finite dimensional

#### Kevin Buzzard (Aug 07 2018 at 20:23):

@Kevin Buzzard can you point me to the relevant files in mathlib for the power series proof please?

data/real/cau_seq.lean and data/real/basic.lean in mathlib are what seem to be the state of the art for sequences. I am not even sure that there is a theory of infinite sums in mathlib, although the definition of a convergent infinite sum (that the finite sums converge) could easily be put into mathlib; the thing is that the moment you put this in, you have to prove a whole bunch of lemmas. Over at the xena project we are a bit less fussy than mathlib, you can look at https://github.com/ImperialCollegeLondon/xena-UROP-2018/tree/master/src/chris_hughes_various/exponential to see some theorems about limits which aren't written in the language of filters and a whole bunch of unofficial theorems like sum of a geometric series written in what might not be the maximal generality.

GT III.5

#### Patrick Massot (Aug 07 2018 at 20:25):

That's how people in the arithmetic and algebraic geometry group talk in Orsay. Except they rather start with AC (yes they refer to the French version too)

Last updated: May 10 2021 at 07:15 UTC