Introducing myself: Winston Yin

Stream: new members

[Winston Yin]

Hi all, my name is Winston Yin, a PhD student in theoretical physics at UC Berkeley. As a side project, I want to contribute to mathlib by formalising some definitions and theorems in algebraic topology and differential geometry. I've just read through the "Theorem Proving in Lean" textbook, so I'm not too familiar with writing non-trivial proofs in Lean yet. Looking at the mathlib index, it looks like there are already some basic definitions, e.g. the smooth fibre bundle. Is there anyone here who's more familiar with this part of mathlib? What would be a good place to start extending mathlib?

[Johan Commelin]

Have you played the natural number game already? It's a great way of getting your hands dirty with Lean proofs. (Of course the maths isn't really exciting if you want to work on AT or DG.)

[Johan Commelin]

For AT, I think we should do some stuff with Kan complexes. I'm not the best expert on what good next steps for DG would be.

[Winston Yin]

Not yet! Where can I find this "game"?

[Alex Zhang]

It's here: http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

[Alex Zhang]

@Winston Yin I am also new to Lean. May I know how long it took you to read through "Theorem Proving in Lean"? Did you try all the exercises on the book?

[Winston Yin]

Ah it looks like the "Theorem Proving in Lean" book already covered a lot of the stuff in the natural number game.

[Winston Yin]

I worked through maybe 60% of the exercises in that book. It took me about 8 days to finish the whole textbook, although I'm on day 7 of quarantine in a hotel room, so I've got all day. It introduces everything from propositional logic, dependent types, proof tactics, inductive types, structure to type classes, so if any thing, it's a good reference.

[Patrick Massot]

You can probably skip this game and go to the tutorial project

[Johan Commelin]

Aah, I thought that "read through" just meant that: reading through. But if you also did the exercise on your lean installation, then you can skip NNG.

[Winston Yin]

Should I care about the difference between Lean 3 and 4? My installation is 3.30.0

[Eric Rodriguez]

they're fairly different, but the main maths library is currently on Lean 3; we're hoping to move over to lean 4 soon™, for some definition of soon

[Winston Yin]

I see. Just curious, what are the todos involved in moving mathlib from Lean 3 to 4? Is Lean 4 not backwards compatible?

[Eric Rodriguez]

Pretty much everything needs to be rewritten, as far as I understand; tactics are different, too, and there is ad-hoc issues with "straight" porting wrt some changes made within Lean 4 specifically.

[Eric Rodriguez]

I am not the best person to ask about this, however; I'm not too involved with Lean 4 right now

[Scott Morrison]

Lean 4 is completely utterly non-backwards compatible. :-) The underlying type theoretic logic is essentially identical, and the syntax is "familiar", but that's about the end of it. That said, there have been a succession of experiments doing semi-automatic translation from Lean 3 to Lean 4, and I understand (second hand!) that hopes remain high that this is viable. It will still involve a lot of human work, however, so don't hold your breath for a mathematics library for Lean 4. I think we're hoping to start by the summer...?

[Eric Rodriguez]

Your summer or northern-hemisphere summer Scott? :b

[Scott Morrison]

That remains to be seen? :-)

[Winston Yin]

Thanks for the info. I'm guessing it is only a coincidence that Scott here is also from down under, and we're not seeing the Australian PM contributing to mathlib in his spare time. :)

[Johan Commelin]

It's his full-time job, isn't it?

[Winston Yin]

I'm using "leanproject new foobar" to create a new project, but failed at step "Failed to download https://oleanstorage.azureedge.net/mathlib/.tar.xz"

[Winston Yin]

Viewing the page in my browser gives a raw XML file with "The specified blob does not exist."

[Johan Commelin]

what does elan show give as output?

[Winston Yin]

installed toolchains

---

stable (default)
leanprover-community/lean:3.30.0

active toolchain

---

stable (default)
Lean (version 3.30.0, commit a5822ea47ebc, Release)

[Johan Commelin]

Weird... it is somehow not fetching the git commit hash from your mathlib clone.

[Johan Commelin]

Is git working properly on your system?

[Winston Yin]

I believe so. I've been using it for other things too

[Winston Yin]

Is it possible this has anything to do with my network connection? I'm in China, and many sites are blocked

[Winston Yin]

I'm on macOS, if that helps at all

[Winston Yin]

Here's the full output of leanproject new mathlib:

cd mathlib
git init -q
git checkout -b lean-3.30.0
Switched to a new branch 'lean-3.30.0'
configuring mathlib 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 160251, done.
remote: Counting objects: 100% (279/279), done.
remote: Compressing objects: 100% (175/175), done.
remote: Total 160251 (delta 178), reused 159 (delta 102), pack-reused 159972
Receiving objects: 100% (160251/160251), 69.51 MiB | 128.00 KiB/s, done.
Resolving deltas: 100% (126322/126322), done.
git checkout --detach fd48ac55697cadbf777009e95b963aa142310a84 # in directory _target/deps/mathlib
HEAD is now at fd48ac556 chore(data/list): extract sublists to a separate file (#7757)
configuring mathlib 0.1
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/.tar.xz to /Users/winston/.mathlib/.tar.xz
Failed to download https://oleanstorage.azureedge.net/mathlib/.tar.xz

[Johan Commelin]

Weird, it prints the commit hash from mathlib.

[Johan Commelin]

Does

wget https://oleanstorage.azureedge.net/mathlib/fd48ac55697cadbf777009e95b963aa142310a84.tar.xz

work?

[Johan Commelin]

(Or another way of downloading that file manually

[Winston Yin]

Yep successfully downloaded

[Winston Yin]

If there's a raw script for leanproject I can continue the remaining steps manually perhaps

[Johan Commelin]

Hmm, I wouldn't know exactly where to look for it.

[Johan Commelin]

But you should be able to unzip that tarball into _target/deps/mathlib inside your project directory.

[Johan Commelin]

The result will be that you have a pre-compiled version of mathlib for your project.

[Winston Yin]

Then are there any subsequent steps that leanproject does?

[Winston Yin]

Hmmm _target/deps/mathlib is already populated

[Winston Yin]

leanproject check says Everything looks fine.

[Bryan Gin-ge Chen]

leanproject is a Python program; the source files are here.

Yes, uncompressing into _target/deps/mathlib should just add a bunch of .olean files there without modifying any of the .lean files.

[Winston Yin]

I see

[Bryan Gin-ge Chen]

Winston Yin said:

Is it possible this has anything to do with my network connection? I'm in China, and many sites are blocked

I do remember that several other people in China have reported having trouble with leanproject in this Zulip chat. I don't know how or if they solved it, but do let us know if you figure something out!

[Winston Yin]

I'm using a special VPN, but that doesn't seem to affect the networking of the terminal. That requires some extra annoying steps. Downloads from github sometimes fails but succeed at slow speed after a couple trials

[Winston Yin]

Now I'm quite sure it's a bug in the python script. Tried in on Ubuntu outside of China as well with same error (Failed to download https://oleanstorage.azureedge.net/mathlib/.tar.xz)

[Winston Yin]

I just went into the python script and manually put in the olean url...

[Winston Yin]

Now what paths should be in lean --path? My VS Code is telling me

file 'topology/basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

[Patrick Massot]

Something really weird is going on here. Obviously the script is failing to build the correct download url.

[Patrick Massot]

Oh I see. You typed leanproject new mathlib so you are trying to make a new project called mathlib. I can believe this totally confuses leanproject.

[Patrick Massot]

What are you actually trying to do here? If you want to work on mathlib itself your should type leanproject get mathlib. If you want to use mathlib in your own project then you should type leanproject new my_shiny_project (or any name by mathlib really).

[Winston Yin]

sigh... after hours I've finally made it work on VS Code. But you're right. I should've been smart and not double named things mathlib

[Winston Yin]

All I wanted to is create a new project. Since my goal is to understand mathlib and extend it, I just called it mathlib. Oh well!

[Winston Yin]

Winston Yin said:

Now what paths should be in lean --path? My VS Code is telling me

file 'topology/basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

Btw for this problem, VSCode should strictly open the directory of the project itself, rather than any parent directory.

[Winston Yin]

So I may be the only one in the world with a working leanproject called mathlib now. Anyway, thanks everyone for your help. You've been exceedingly generous

[Johan Commelin]

Well, many people have a working lean project called mathlib (-; But it's a very different project than yours :rofl:

[Patrick Massot]

Yes, we don't know how to write this more clearly in the instructions, but many people still fall in this trap. I thought that the Lean VSCode extension even has a warning if you open the wrong folder. But it probably triggers only if you open a child of the right folder, not a parent.

[Winston Yin]

I actually started writing Lean code in VS Code even before installing mathlib, so it just got stuck in the parent directory without a retrospective warning

[Winston Yin]

If I follow a particular undergraduate / graduate level textbook when formalising a certain area, the definitions and theorems are often not as general as they can be. Is there any harm in formalising the less general statements, in that they might be superseded in the future by more knowledgeable mathematicians? E.g. undergraduate textbooks are going to prove things for groups rather than monoids, or vector spaces instead of modules.

[Andrew Ashworth]

The ghost of Plato will haunt you if you don't write code in the perfect generality.

[Alex J. Best]

There is no real harm, the only problem is that if you write statements that could be more general, and someone later tries to find the general version and doesn't (e.g. via tactic#library_search) they may end up reproving the fact which wastes a little bit of time. Also: as the person writing the first version it may take you less time to generalise the lemma than someone else to later as you understand the proof best at the time of writing, so if there are things that become clear can be improved during the proof, I'd say go for it. Mathlib tries to be quite general, but there are a lot of statements in mathlib that nevertheless get added in a more specific form (and then maybe generalised later).

[Alex J. Best]

One of the many benefits of formalization is often how easy generalization can be, Lean can find the gaps in a long proof (assuming it is already written in lean) after an assumption is changed far faster than a human. So often generalizing using Lean is just a case of editing an assumption, jumping to the lines that broke and fixing those then being told by lean that the proof works again.

[Scott Morrison]

This happens all the time. One thing that can be useful is to briefly outline what you plan to formalise in a thread here, and ask how it looks. (I often try to write new developments by writing definitions and statements first, and leaving all the proofs as sorry --- when you reach that stage is an excellent time to ask for advice.) People can often tell you about useful existing work, or point out cheap generalizations. It's also fine, if someone says "oh, with bronchial azumaya tapestries this is just a special case of ...", to say "err, I'd prefer to keep it simple". That is, if someone suggests a big generalization that is beyond what you know about / want to know about, it's fine to suggest they do it in a later PR. :-)

[Winston Yin]

That's very helpful. If I understand Alex correctly, I can naively follow the (potentially less general) statements in the textbook first, prove what I need to prove, and then see if generalisation breaks the proof. I'm seeing a lot of algebra results formalised from Bourbaki, and it's just a bit intimidating.

[Johan Commelin]

On the other hand, Lean also teaches us that with the correct generalization, proofs can become genuinely simpler. This is something to keep in mind.

[Winston Yin]

I've been reading a lot of the definitions on mathlib, and I'm trying to understand the conceptual difference between structure new_struct (S : Type*) [old_class S] and structure new_struct (S : Type*) extends old_class S. What are the technical differences between them, and why would one choose one over the other?

[Kevin Buzzard]

The question is whether you want [new_struct X] to give you an instance of [old_class X] or to demand one.

[Kevin Buzzard]

For example, if I say [ring X] should Lean say "wait a minute, a ring is an add_comm_group so you need to type [add_comm_group X] first (no) or should it say "OK I will assume you want X to be an add_comm_group given that you just told us you want it to be a ring" (yes)

[Kevin Buzzard]

Conversely, if I want to say that M is a Noetherian R-module then I'm not sure that is_noetherian R M should automatically make R into a ring, because maybe I want it to be a field or a semiring. I'd rather do [field R] first so I have better control over exactly what I want here.

[Winston Yin]

Let me carefully think about these two examples.

[Scott Morrison]

One reason to prefer [old_class S] is that if we have both new_struct and new_struct_2 which both extend old_class, then there is no mechanism to say that they both extend it in the same way, so you can't have both without introducing a bad ambiguity.

[Scott Morrison]

A reason to not prefer [old_class S] is that you end up with large numbers of typeclass arguments.

[Winston Yin]

Ok it took me a while to think about this. Is this understanding correct: When I make a ring X, all I'm doing is use the same constructors for add_comm_group, plus some additional ones. That's why ring extends add_comm_group. On the other hand, when I'm trying to make a subring X, assuming there's an instance of [ring X], I just want to show all the closure statements, without having to go through a million constructors under ring. This is why subring X doesn't extend ring X. The property that any R : subring X is also a ring R.carrier is now a separate theorem that's also an instance accessible to the type class system.

[Winston Yin]

A separate question is whether one should define an object like the reals directly as a ring or as a Type that has some instances available when we use it as a ring, or a field/group/monoid/etc. In the case of the reals we should probably NOT implement it as a ring. But it would in principle still be permissible to implement it as a ring, and then define some instances to show it can also be used as a field/group/monoid. Is this correct?

[Kevin Buzzard]

These decisions about how to set things up aren't somehow intrinsic to the type theory, they are design decisions which have been made by the maths library. I don't know what you mean by "we should NOT implement [the reals] as a ring". There is a term of type ring real in the type class inference system.

import data.real.basic

example : ring ℝ := infer_instance

[Winston Yin]

I see. Thinking about it as a design decision makes sense to me. I'm sure with more practice, I'll see the benefit of either in various situations. Thank you!

[Huỳnh Trần Khanh]

hey @Winston Yin what do you mean by either? I don't quite understand what you are trying to convey lol

[Huỳnh Trần Khanh]

I'm also confused by the not implement as a ring part

[Winston Yin]

Sorry! While trying to clarify myself, I realised the two approaches I described are essentially the same implementation. The difference in my mind was whether real : ring cauchy_seq, where cauchy_seq : Type is separately constructed, or real : Type, and then a ring real is constructed from real. It's just a matter of naming.

[Winston Yin]

Winston Yin said:

Ok it took me a while to think about this. Is this understanding correct: When I make a ring X, all I'm doing is use the same constructors for add_comm_group, plus some additional ones. That's why ring extends add_comm_group. On the other hand, when I'm trying to make a subring X, assuming there's an instance of [ring X], I just want to show all the closure statements, without having to go through a million constructors under ring. This is why subring X doesn't extend ring X. The property that any R : subring X is also a ring R.carrier is now a separate theorem that's also an instance accessible to the type class system.

But does ^ this description make sense as a design decision?

[Johan Commelin]

What you quoted is correct. But I'm not sure it captures the design decision around [foo X] vs extends foo X.

[Johan Commelin]

Think about commutative groups. There are two ways to think about this. You can think of "commutative group" as an atom: [comm_group G]. Or you can think of "commutative" as an extra property on top of "group": [group G] [is_commutative G]

[Johan Commelin]

So you can define

class comm_group (G : Type*) extends group G :=
(mul_comm : ...)

or

class is_commutative (G : Type*) [group G] :=
(mul_comm : ...)

[Johan Commelin]

The difference is that

1. comm_group G contains data, but is_commutative G does not. This is an important difference in the practice of formalization.
2. [comm_group G] is a bit shorter to write than [group G] [is_commutative G]
3. comm_group G asks the type class system to search for 1 thing, whereas the other approach needs 2 searches.

[Winston Yin]

I see! That's very illustrative

[Winston Yin]

When invoking [is_commutative G], the type class system won't automatically include [group G], even though that's in the definition of is_commutative?

[Winston Yin]

What would happen if I write example (G : Type) [is_commutative G] : ... := ...

[Johan Commelin]

you would get an error

[Johan Commelin]

that it can't find [group G]

[Winston Yin]

This is why Scott said earlier that there could be a lot of [...] if one does not use extends

[Winston Yin]

Thanks for the example!

[Winston Yin]

How does one type the lift coercion symbols? ↑↥⇑

[Bryan Gin-ge Chen]

↑: \u, ↥: \u-|, ⇑: \u= or \Uparrow.

The full list of abbreviations is here. Also, if you hover over a symbol in VS Code, the extension should pop up a window with the shortcuts.

[Winston Yin]

If I'm sick and tired of writing

  {G : Type _} [group G]
  {R : Type _} [semiring R]
  {M : Type _} [add_comm_monoid M] [module R M]

in front of every definition and theorem, is there a way to condense all this, say, for the whole namespace?

[Andrew Ashworth]

The variable keyword?

[Winston Yin]

Any way to include the [group G] and so on using the variable keyword?

[Kevin Buzzard]

Take a look at all the library files you're importing by right clicking on one

[Winston Yin]

It looks like {G : Type _} {R : Type _} {M : Type _} can be in variable, but the [group G] and so on have to be written explicitly in every def and theorem. Is that correct?

[Johan Commelin]

@Winston Yin

variables {G : Type _} [group G] {R : Type _} [semiring R] {M : Type _} [add_comm_monoid M] [module R M]

[Winston Yin]

Ok let me try this

[Winston Yin]

I see. I was missing an "s" in variables. Silly!

[Mario Carneiro]

you can also write

variable {G : Type _}
variable [group G]
variable {R : Type _}
...

but that style is not very common

[Winston Yin]

If we have N : submodule R M and a linear map f : M -> M' between module R M and module R M', are there existing definitions and theorems for the image of N under f as im_f_N : submodule R M' and for the induced linear map f' : N -> im_f_N?

[Winston Yin]

I think I found it: submodule.map

[Johan Commelin]

I think docs#submodule.subtype or docs#submodule.incl is the induced map

[Winston Yin]

There is submodule.module, which turns a submodule into a module. But is there a function or easy way that takes a module and returns itself as a submodule of itself? (Same for groups/subgroups, etc)

[Johan Commelin]

\top is the "object viewed as subobject of itself"

[Johan Commelin]

If lean is confused about which variant of \top you mean, you can give it a hint (\top : submodule R M)

[Winston Yin]

Got it. Thanks for the quick reply!

[Johan Commelin]

Similarly \bot is the zero submodule/group/algebra/etc

[Winston Yin]

I'm scratching my head here. I'm trying to state a theorem:

theorem range_restrict_eq {R : Type _} [semiring R]
  {M : Type _} [add_comm_monoid M] [module R M]
  {N : Type _} [add_comm_monoid N] [module R N]
  (f : N →ₗ[R] M) : ∀ x : N, f x = f.range_restrict x

Basically, if the codomain of the f has been restricted to be its range, then f and its restriction are equal in value. This is stated for linear maps f. (If such a thing already exists, please let me know.) The written code returns no error. Lean even tells me the goal with all the coe's written out: ⇑f x = ↑(⇑(f.range_restrict) x).

But when I flip LHS and RHS of the equality (f.range_restrict x = f x), the following error is shown:

type mismatch at application
  ⇑(f.range_restrict) x = ⇑f x
term
  ⇑f x
has type
  M
but is expected to have type
  ↥(f.range)

Errors are shown even when I put in the explicit arrows in the original direction ⇑f x = ↑(⇑(f.range_restrict) x) and in the opposite direction ↑(⇑(f.range_restrict) x) = ⇑f x. What is going on?

[Scott Morrison]

Lean is working out the type involved in the equality by looking at the first argument.

[Winston Yin]

First argument meaning the whole LHS of equality?

[Scott Morrison]

As you've written it above, that is M, so when if reached f.range_restrict x, Lean thinks "that doesn't look right, it's in f.range, not in M", and goes looking for a coercion to fix the problem, which is successfully finds.

[Scott Morrison]

If you switch the order, Lean decides the equality is an equation in f.range.

[Scott Morrison]

When it reaches f x it says "that doesn't look right", and goes looking unsuccessfully for a coercion from M to f.range.

[Scott Morrison]

You can fix this by stating the conclusion as (f.range_restrict x : M) = f x.

[Winston Yin]

Indeed that fixes it. Let me think like Lean for a moment

[Winston Yin]

Even with explicit arrows given, Lean still uses the preceding context to guess the target of the coe. Is that right?

[Winston Yin]

Your explanation makes sense, but why ⇑f x = ↑(⇑(f.range_restrict) x) fails still doesn't

[Scott Morrison]

I would guess because pretty printing is not always round-trippable, and Lean can't work out where the arrows are intended to send things. I haven't look closely, however.

[Scott Morrison]

Generally, when copy-and-pasting goals with arrows, you may need to replace arrows with explicit coercions: (X : T).

[Winston Yin]

I see. Learned something new!

[Winston Yin]

And I think I found the theorem that's identical to the one I stated: linear_map.cod_restrict_apply, though it wasn't obvious before I saw the pretty printed statement

[Winston Yin]

Suppose I'm trying to prove example (m n : ℕ) (h : m = n) (f g : ℕ → ℕ) : f (g m) = f (g n) := using tactics. I can give a one line proof exact congr_arg f (congr_arg g h), but how can I prove this more naturally in two step, first showing g m = g n, and then showing the ultimate goal?

[Winston Yin]

Sorry this sounds quite basic

[Scott Morrison]

by subst h?

[Scott Morrison]

Are you asking about the have tactic?

[Winston Yin]

How would I continue this: have congr_arg g h when I've already given it the term I want...

[Winston Yin]

My original thought was to rewrite the hypothesis using congr_arg

[Winston Yin]

Until my hypothesis looks like my goal

[Eric Wieser]

have := congr_arg g h, exact congr_arg f this

[Winston Yin]

Thanks!

[Winston Yin]

Looks like I mixed up the syntax between the have in tactic mode and in term mode

[Winston Yin]

I see that is_subgroup is deprecated. What is it replaced by?

[Patrick Massot]

docs#subgroup

[Winston Yin]

So no more implicit coercions into subgroups?

[Kevin Buzzard]

You can use is_subgroup, but the community's conclusion on the matter is that subgroup is simply more convenient in practice, in most cases.

[Winston Yin]

I see. Thanks

[Kevin Buzzard]

I guess mathematically the argument could be something like this: when do you ever get a set, and then later on prove that it's a subgroup? Of course this happens, but why does it happen? It happens because the set is actually a kernel or an image or a product or... of subgroups, so actually the myriad constructors of subgroups which we have seem to suffice.

[Scott Morrison]

But for those rare occasions when you discover an entirely novel way to build a subgroup, there's still is_subgroup. :-)

[Scott Morrison]

(I feel like this should be something like discovering a new small mammal...)

[Winston Yin]

I'm still practising Lean by defining and proving random things about groups, homomorphisms, and linear maps (often discovering equivalent theorems in mathlib afterwards), but I'm already eager to contribute new definitions and theorems in whichever area I'm more familiar with. One area might be the representation theory of finite groups and semisimple Lie algebras, which I learned from Fulton & Harris. To what extent is this formalised, and would following a non-specialist book like Fulton & Harris be a problem down the road?

[Winston Yin]

(Many harder theorems are stated without proof in that book, but I'm just going to focus on the easier bits for now.)

[Winston Yin]

I guess I'm pretty lost as to where to begin

[Winston Yin]

If I write a bunch of definitions that later turn out to be a special case of something in mathlib, would that still be worth it, and would it be possible to then state them as a special case after the fact?

[Kevin Buzzard]

I think it might be best if you started asking questions new threads with appropriate topics

[Kevin Buzzard]

There's plenty of Fulton-Harris which isn't in Lean and it would be an excellent thing to formalise.

[Winston Yin]

Sorry, I'm new to Zulip as well.

[Kevin Buzzard]

Start a Fulton-Harris thread in #maths and we can talk there. People interested in it might well not see the conversation if it's hidden in this thread.

[Scott Morrison]

I think Fulton and Harris, while a lovely book for humans to learn from, is pretty terrible from a formalisation point of view. :-)

Formalisation of representation theory will work best if we have a solid base of representation theory of algebras, before groups / finite groups / Lie algebras etc are mentioned. This makes sure we don't end up doing the same things over and over again. Fulton and Harris is somehow exactly backwards in this respect.

I really Etingof's Representation Theory book (freely available on his website?). I think it's both pretty friendly to humans, and follows a path that would be productive in mathlib.