## Stream: maths

### Topic: stuff we want

#### Kevin Buzzard (Apr 14 2019 at 12:18):

I think it's time to update

https://github.com/leanprover-community/mathlib/blob/master/docs/wip.md

and it's also perhaps a good idea to write a list of stuff which we'd like to have in mathlib.

Everyone -- what maths would you like to see in mathlib? Some ideas are on the mathoverflow question -- which ones should be listed as "todo"? Are we ready for manifolds next? I don't know enough about the state of multivariable calculus in Lean to know how ready we are.

@Kenny Lau @Scott Morrison @Reid Barton @Chris Hughes @Patrick Massot @Sean Leather could you give me an update for these former WIPs? Did they happen? Will they happen? Shall I delete or edit those entries?

We should mention the work of @Jeremy Avigad and others on differentiable functions I guess.

I don't think we have power series in 1 variable (although it's easier to code than polynomials in one variable!), and I don't think we have the basic theory of Dedekind domains; both of these should be easily accessible nowadays.

#### Patrick Massot (Apr 14 2019 at 19:24):

I think it's time either get rid of that page or find someone who wants to take responsibility to update it. You can remove the line about calculus, and maybe indicate that Sébastien is working on manifolds.

#### Patrick Massot (Apr 14 2019 at 19:25):

The documentation about what is already covered is also badly out of date, but I certainly intend to work on this once my teaching semester will be over

#### Jeremy Avigad (Apr 14 2019 at 21:57):

I don't have an opinion on how / whether to maintain that page, but I thought I would mention that a student here, Zhouhang (Joe) Zhou, has started working on integration. He is aiming to define the Bochner integral following advice from Johannes. If all goes well, the plan is to also prove suitably general versions of the FTC to link integration and differentiation.

#### Scott Morrison (Apr 14 2019 at 22:48):

I agree we should get rid of that page, but I would really love to replace it with something better.

#### Scott Morrison (Apr 14 2019 at 22:49):

One option is to use the issues list on leanprover-community/mathlib.

#### Scott Morrison (Apr 14 2019 at 22:49):

We could tag things as "bug", "chore", "roadmap", "easy", "medium", "good-first-PR", etc.

#### Scott Morrison (Apr 14 2019 at 22:51):

Another option is trello, a "kanban board" app. I've used it in the past; it's very nice to use, but doesn't magically solve the problem of needing a commitment from a enough people to actually use it.

#### Scott Morrison (Apr 14 2019 at 22:53):

It seems there are reasonable integrations with zulip, github, and vscode.

#### Joseph Corneli (Apr 15 2019 at 11:39):

I think it would be great to have some more tutorials (_target/deps/mathlib/docs/tutorial/) so that the features that exist already (and new ones that are developed) are easier to understand.

#### Scott Morrison (Apr 15 2019 at 12:08):

I just added a tutorial to #938, mostly demonstrating how far we have to go. :-)

#### Adrian Chu (Apr 21 2019 at 04:50):

Are ordinal numbers and cardinal number formalized yet?

yes

#### Mario Carneiro (Apr 21 2019 at 04:50):

set_theory.ordinal and set_theory.cardinal

#### Mario Carneiro (Apr 21 2019 at 04:52):

no surreals, go for it

#### Kevin Buzzard (Apr 21 2019 at 05:03):

There are hyperreals!

#### Kevin Buzzard (Apr 21 2019 at 05:05):

That Conway stuff -- I went back to Conway's book, and he's clearly aware of the foundational issues surrounding his constructions of numbers and games. It seems to me that these definitions are proper classes. Hence I would expect to be able to define a game recursively like before, except only using subsets of Game from Type 0 in some sense -- I want to stop the diagonalisation argument from failing because of ulift issues. Is this possible?

#### Adrian Chu (Apr 21 2019 at 05:07):

each individual surreal number is a set, but the collection of all surreals is a class

#### Mario Carneiro (Apr 21 2019 at 05:07):

lean doesn't do classes, it does universe parametric types

#### Mario Carneiro (Apr 21 2019 at 05:08):

ordinal.{u} : Type (u+1)

#### Kevin Buzzard (Apr 21 2019 at 05:08):

inductive game : Type
| intro : Π L R : list game, game


This was Scott's original formalization of Conway's notion of a game.

#### Kevin Buzzard (Apr 21 2019 at 05:10):

This version

import data.finset

inductive game : Type
| intro : Π L R : finset game, game


is maybe not inconsistent, but is not strong enough to capture Conway's powerful notion.

#### Kevin Buzzard (Apr 21 2019 at 05:11):

Mario's diagonalisation argument is here:

import logic.function

constant game : Type
constant game.intro : set game → set game → game
constant {u} game.rec {C : game → Sort u} :
(∀ L R, C (game.intro L R)) → ∀ g, C g
axiom {u} game.rec_eq {C : game → Sort u}
(H : ∀ L R, C (game.intro L R)) (L R) :
game.rec H (game.intro L R) = H L R

def game.right : game → set game := game.rec (λ L R, R)
theorem game.right_eq (L R) : (game.intro L R).right = R := game.rec_eq _ _ _

example : false :=
@function.cantor_injective game (game.intro ∅) $λ R R' e, (game.right_eq ∅ _).symm.trans$
(congr_arg game.right e).trans (game.right_eq ∅ _)


#### Kevin Buzzard (Apr 21 2019 at 05:12):

So it seems to me that thus far we have failed to define a Conway game in Lean and I for one am unsure how to proceed.

#### Keeley Hoek (Apr 21 2019 at 05:14):

What if games take a universe parameter

#### Keeley Hoek (Apr 21 2019 at 05:14):

And their "inner games" are one universe lower

#### Mario Carneiro (Apr 21 2019 at 05:17):

inductive {u} pSurreal : Type (u+1)
| mk : ∀ α β : Type u, (α → pSurreal) → (β → pSurreal) → pSurreal


I'm reading the definition of le, well formed, and the equivalence relation, and it's a complicated mutual induction, but this is the basic structure

#### Kevin Buzzard (Apr 21 2019 at 05:17):

And what happens to the diagonal argument?

#### Mario Carneiro (Apr 21 2019 at 05:17):

they are well founded just as in Conway's construction

#### Mario Carneiro (Apr 21 2019 at 05:18):

you can't make a surreal number from any set of surreal numbers, only a set composed of previously constructed surreals

#### Kevin Buzzard (Apr 21 2019 at 06:49):

Here's where I get stuck trying to prove false:

type mismatch at application
pSurreal.mk ↥∅ (subtype R)
term
subtype R
has type
Type (?+2) : Type (max 1 (?+3))
but is expected to have type
Type (?+1) : Type (?+2)


#### Kevin Buzzard (Apr 21 2019 at 06:50):

Given an arbirtrary R, I can't convince Lean that it's come from the universe below.

#### Kevin Buzzard (Apr 21 2019 at 06:50):

Oh but this is great! There are a ton of things one can prove about that structure!

#### Mario Carneiro (Apr 21 2019 at 07:35):

I have a definition of the order:

inductive {u} pSurreal : Type (u+1)
| mk : ∀ α β : Type u, (α → pSurreal) → (β → pSurreal) → pSurreal

namespace pSurreal

def le_lt (x y : pSurreal) : Prop × Prop :=
begin
induction x with xl xr xL xR IHxl IHxr generalizing y,
induction y with yl yr yL yR IHyl IHyr,
exact (
(∀ i, (IHxl i ⟨yl, yr, yL, yR⟩).2) ∧ (∀ i, (IHyr i).2),
(∃ i, (IHxr i ⟨yl, yr, yL, yR⟩).1) ∨ (∃ i, (IHyl i).1))
end

instance : has_le pSurreal := ⟨λ x y, (le_lt x y).1⟩
instance : has_lt pSurreal := ⟨λ x y, (le_lt x y).2⟩

@[simp] theorem mk_le_mk {xl xr xL xR yl yr yL yR} :
(⟨xl, xr, xL, xR⟩ : pSurreal) ≤ ⟨yl, yr, yL, yR⟩ ↔
(∀ i, xL i < ⟨yl, yr, yL, yR⟩) ∧
(∀ i, (⟨xl, xr, xL, xR⟩ : pSurreal) < yR i) := iff.rfl

@[simp] theorem mk_lt_mk {xl xr xL xR yl yr yL yR} :
(⟨xl, xr, xL, xR⟩ : pSurreal) < ⟨yl, yr, yL, yR⟩ ↔
(∃ i, xR i ≤ ⟨yl, yr, yL, yR⟩) ∨
(∃ i, (⟨xl, xr, xL, xR⟩ : pSurreal) ≤ yL i) := iff.rfl

def equiv (x y : pSurreal) : Prop := x ≤ y ∧ y ≤ x

def ok : pSurreal → Prop
| ⟨l, r, L, R⟩ :=
(∀ i j, L i < R j) ∧ (∀ i, ok (L i)) ∧ (∀ i, ok (R i))

end pSurreal


Proving that it's a good ordering is a mess though

#### Adrian Chu (Apr 21 2019 at 08:53):

btw is galois theory done?

nope

#### Mario Carneiro (Apr 21 2019 at 10:15):

@Kevin Buzzard I extended the surreal number stuff into PR #958 . Maybe this is an interesting project for some of your minions.

#### Kevin Buzzard (Apr 21 2019 at 13:54):

Scott has minions too. I already mentioned it to mine. They're all busy revising

#### Kevin Buzzard (Apr 21 2019 at 15:02):

Some students at Imperial did a bunch of Galois theory stuff but it's not yet finished. I believe we still don't have algebraic closure but we might have the main basic theorem about normal extension = splitting field IIRC

#### Adrian Chu (Apr 21 2019 at 15:36):

i see. how about representation theory?

Nothing

#### Kevin Buzzard (Apr 21 2019 at 15:37):

We're just getting to the point where we can think about this stuff; we only got rings and modules working a few months ago. There were technical implementation issues involved in translating stuff into Lean's dependent type theory.

i see...

#### Kevin Buzzard (Apr 21 2019 at 15:38):

The first implementation had a module attached to the ring it was a module over, and then in practice it turned out that we were constantly thinking of modules as modules over more than one ring at once, so it had to be re-done with the ring being given as an extra parameter

#### Kevin Buzzard (Apr 21 2019 at 15:39):

They're clearly accessible, it's just that nobody did them yet. Imperial undergraduates might do it if you give them a year or so.

#### Adrian Chu (Apr 21 2019 at 15:42):

is there anything that imperial undergrads have already that is not yet in mathlib?

#### Kevin Buzzard (Apr 21 2019 at 16:05):

Yes, they develop stuff and put it in all sorts of random places.

#### Kevin Buzzard (Apr 21 2019 at 16:06):

@Chris Hughes and @Kenny Lau are the people to talk to about the current state of Galois theory and the like, but they have exams in a couple of weeks so might not be checking the chat so much.

#### Adrian Chu (Apr 23 2019 at 16:24):

are homotopy groups done?

#### Kevin Buzzard (Apr 23 2019 at 16:44):

A student of mine did pi_1 but I don't think it made it into mathlib, so whilst there might be some code to work on, it might need work before it is in a fit state for the maths library. @Reid Barton is probably the person to ask about higher homotopy groups

#### Johan Commelin (Apr 23 2019 at 17:18):

@Adrian Chu A bachelor student in Freiburg is about to start a project on pi_n

#### Johan Commelin (Apr 23 2019 at 17:19):

I have code for simplicial sets, and we want to clean that up and define higher pi_n

#### Adrian Chu (Apr 24 2019 at 04:00):

I found this (https://github.com/rwbarton/lean-homotopy-theory/tree/lean-3.4.2/src/homotopy_theory/topological_spaces) by Reid Barton. He has weak homotopy equivalence too.

#### Johan Commelin (Apr 24 2019 at 04:21):

Yup, Reid has written enormous amounts of code. I haven't yet read all of it...

#### Kevin Buzzard (Apr 24 2019 at 04:40):

@Reid Barton this code will presumably begin to rot if you don't get it into mathlib...

#### Adrian Chu (Apr 24 2019 at 04:42):

May I ask what the procedure of getting a proof into matlib is?

#### Kevin Buzzard (Apr 24 2019 at 04:48):

you PR it on github

#### Kevin Buzzard (Apr 24 2019 at 04:48):

and then it goes through a review process

#### Adrian Chu (Apr 24 2019 at 15:03):

What geometric objects do we currently have? Spheres? Balls?

nothing :-)

#### Greg Conneen (Apr 25 2019 at 00:37):

Is any of that actually hard to create though? Maybe it'd be useful to have balls defined, as that could lend itself naturally to a lot of analysis, especially dealing with manifolds

#### Greg Conneen (Apr 25 2019 at 00:37):

Speaking of which, do we have anything on manifolds?

#### Johan Commelin (Apr 25 2019 at 02:36):

Mathlib doesn't currently have anything on manifolds. But both @Patrick Massot and @Sebastien Gouezel made a start, and there is good reason to hope that their combined efforts will lead to a nice library on manifolds in the (near?) future...

#### Kevin Buzzard (Apr 25 2019 at 04:43):

Is any of that actually hard to create though?

Nothing is impossible, but everything is harder than you think, at least initially. For example someone was asking about partitions of unity. In theory this sounds fine, but then you realise that if you want to use C^infty functions, you will need to prove stuff like the sum and the product of C^infty functions is C^infty, and this is not hard, you prove that the sum and the product of C^n functions is C^n and then use induction on n, and after a while of doing all this you realise that actually it's not hard but sometimes it's just a lot of work. Even after you built bump functions you still have to make them usable, by making an API for them, and sometimes it's hard to work out what this API should even be until you start to apply your theory to do something else, and suddenly you need things like "if I have two partitions of unity then I can put them together and get a third one", and then you realise you need to prove that $(\Sigma_i f_i)(\Sigma_j g_j)=\Sigma_{i,j}f_ig_j$ and then you discover that for C^infinity functions this is only in the library for finite sums, and you have an infinite but locally finite sum, so now you need to do more basic stuff etc etc.

Nothing is hard, but until all the basics are done there will be plenty of things left which are an annoying struggle. Once an entire undergraduate pure mathematics syllabus is done, things will start getting easier.

LOL

#### Adrian Chu (Apr 25 2019 at 05:16):

maybe a topological manifold is easier..

#### Kevin Buzzard (Apr 25 2019 at 05:18):

The correct thing to do is to do the work and make the API. Someone has to do it. The computer scientists don't know what a partition of unity is, but if you write some crappy code which implements it then they can look at it and change it and make it much better and get it mathlib-ready, if they have the time.

#### Adrian Chu (Apr 25 2019 at 05:22):

actually who are the computer scientists here? Or, who is responsible for maintaining mathlib?

#### Kevin Buzzard (Apr 25 2019 at 05:30):

Mathlib is maintained by the maintainers -- you can probably look on the githib page if you understand githib to see who they are. The people who have contributed the most to mathlib is certainly something you can see on github. Mario and Johannes wrote a lot of it originally -- this was the more CS stuff. Now more and more mathematicians are getting involved, but at the minute we write code like Noetherian rings, and they look at it and ask us questions about our use cases and then write better code for us which does the same thing. At some point they'll not understand the maths any more, and then it's up to us to write our own good code.

#### Kevin Buzzard (Apr 25 2019 at 05:31):

But hopefully by then we have such a good API for basic maths that writing good code is not so hard.

#### Mario Carneiro (Apr 25 2019 at 05:46):

I don't understand the math books or whatever you are using to derive the things you write, but I do understand the lean code. When reading high end mathematics that's been formalized, the tricky part is figuring out the motivation for stuff, and figuring out what was meant when something goes wrong and the intent isn't clear

#### Adrian Chu (Apr 25 2019 at 07:22):

is the corresponding question to group know?

#### Adrian Chu (Apr 25 2019 at 07:23):

(ignore the above comment)

#### Mario Carneiro (Apr 25 2019 at 07:24):

there is a delete button

#### Sebastien Gouezel (Apr 25 2019 at 14:34):

Any possibility to get #955 merged in the near future, by the way? I need this (and then #956) to submit more material on differentiation and higher order derivatives. I think Mario was happy with it, but maybe there is still something to be improved.

#### Jeremy Avigad (Apr 25 2019 at 17:30):

I think Mario was happy with it and I don't see any problems, so I marked it ready to merge.

Last updated: May 09 2021 at 09:11 UTC