things to formalise

Stream: maths

[Edward Ayers]

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]

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

[Patrick Massot]

is the main place

[Edward Ayers]

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

[Patrick Massot]

see also https://www.youtube.com/watch?v=5tS4j_A1ZvU

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

The chain rule is waiting for the norms PR

[Kevin Buzzard]

What is the problem with the norms PR?

[Patrick Massot]

Mario and Johannes want to work on it

[Patrick Massot]

that's all I know

[Edward Ayers]

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

[Johan Commelin]

I don't think power series are in mathlib.

[Johan Commelin]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

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]

@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.

[Patrick Massot]

GT III.5

[Patrick Massot]

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)