stuff we want

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

I think writing a few "roadmaps" would be really helpful.

[Joseph Corneli]

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]

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

[Adrian Chu]

Are ordinal numbers and cardinal number formalized yet?

[Mario Carneiro]

yes

[Mario Carneiro]

set_theory.ordinal and set_theory.cardinal

[Adrian Chu]

how about surreal numbers? lol

[Mario Carneiro]

no surreals, go for it

[Kevin Buzzard]

There are hyperreals!

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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]

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]

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]

What if games take a universe parameter

[Keeley Hoek]

And their "inner games" are one universe lower

[Mario Carneiro]

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]

And what happens to the diagonal argument?

[Mario Carneiro]

they are well founded just as in Conway's construction

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

btw is galois theory done?

[Mario Carneiro]

nope

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

i see. how about representation theory?

[Kevin Buzzard]

Nothing

[Kevin Buzzard]

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.

[Adrian Chu]

i see...

[Kevin Buzzard]

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]

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]

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

[Adrian Chu]

have already done*

[Kevin Buzzard]

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

[Kevin Buzzard]

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

are homotopy groups done?

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Adrian Chu]

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]

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

[Kevin Buzzard]

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

[Adrian Chu]

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

[Kevin Buzzard]

you PR it on github

[Kevin Buzzard]

and then it goes through a review process

[Adrian Chu]

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

[Kevin Buzzard]

nothing :-)

[Greg Conneen]

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]

Speaking of which, do we have anything on manifolds?

[Johan Commelin]

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]

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.

[Adrian Chu]

LOL

[Adrian Chu]

maybe a topological manifold is easier..

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

is the corresponding question to group know?

[Adrian Chu]

(ignore the above comment)

[Mario Carneiro]

there is a delete button

[Sebastien Gouezel]

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]

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