Zulip Chat Archive

Stream: new members

Topic: greetings & where to start?

Vasily Nesterov (Nov 03 2022 at 18:31):

Hi everyone! I am a third year student in Math & CS and I really enjoy playing with Lean.

Maybe I can bring some benefit to the community? I have seen the page https://leanprover-community.github.io/undergrad_todo.html about undergraduate topics still uncovered in mathlib, and I want to work on some of them. I have checked the PR list and, for example, the following topics do not seem to be done:

  1. Matrices: Jordan normal form
  2. Fourier analysis: Dirichlet theorem, Fejer theorem, Plancherel’s theorem.
  3. ODE: exit theorem of a compact subspace, stability of equilibrium points (linearisation theorem), linear differential systems, etc

I just want to become more familiar with mathlib and lean and would be happy to pick any of them. I will be grateful if someone would outline the situation in these subjects and give advice on how and where to start.

Kevin Buzzard (Nov 03 2022 at 22:55):

The undergrad_todo is a place where new members sometimes go to die :-( There is often a reason these things are not yet done, perhaps the community demands that they're done in a specific way and an expert is needed :-/

Patrick Massot (Nov 03 2022 at 23:28):

Don't listen to Kevin, there are many things that are still doable on this list. Many items are not done because they are boring elementary mathematics.

Moritz Doll (Nov 03 2022 at 23:43):

There is also a tag on the issue tracker on github for good beginner projects: https://github.com/leanprover-community/mathlib/issues?q=is%3Aissue+is%3Aopen+sort%3Aupdated-desc+label%3Agood-first-project

Moritz Doll (Nov 03 2022 at 23:47):

From undergrad_todo, the special orthogonal/unitary groups should be rather easy and there are examples of matrix groups that you could follows. Looking at docs#matrix.special_linear_group and docs#matrix.orthogonal_group should suffice to implement matrix.special_orthogonal_group

Moritz Doll (Nov 03 2022 at 23:49):

btw: why is the special linear group still on the list? there is docs#matrix.special_linear_group

Moritz Doll (Nov 03 2022 at 23:55):

@Fourier Series: There was the idea to rewrite the Fourier series, but I don't know what became out of that. If you are interested in working on that you should ping Heather Macbeth and you might have to do some refactoring of existing code. So it might take a some time to get to the interesting parts, but if you really want to learn Lean, then it can be worthwhile.

Yaël Dillies (Nov 04 2022 at 06:00):

Moritz Doll said:

btw: why is the special linear group still on the list? there is docs#matrix.special_linear_group

Probably same answer as here, unless you have more to say, @Heather Macbeth?

Kevin Buzzard (Nov 04 2022 at 07:54):

I think that the truth is that there might be some items on there which are accessible (as well as some items which are not at all accessible to beginners but which look accessible, which is very disheartening) but there problem is that the more detailed descriptions of what needs doing and how the mathlib community want it done are often described in threads like this which are transient and get lost. My main point is that it's not like 2-3 years ago where people could just say "oh you don't have X, here I can do X" and then they do X and get it merged. It's now much more complicated which is why the list has stagnated.

Kevin Buzzard (Nov 04 2022 at 07:55):

Newcomers stumble onto the list but not the details of what we know needs actually doing.

Kevin Buzzard (Nov 04 2022 at 07:56):

There's an undergraduate at Imperial who has essentially done partial factions by the way. Should I record this somewhere as WIP?

Moritz Doll (Nov 04 2022 at 08:05):

In my opinion the github issue tracker is way better for maintaining a list of "beginner issues". The problem with the undergrad list is as you say that "mathematically easy" != "Lean easy".

Moritz Doll (Nov 04 2022 at 08:07):

As for the partial fractions: if the student is ok with it, then you could create a WIP PR and tag it with "please-adopt"

Henrik Böving (Nov 04 2022 at 17:53):

Patrick Massot said:

Don't listen to Kevin, there are many things that are still doable on this list. Many items are not done because they are boring elementary mathematics.

I barely even know the terms on the list /o\

Vasily Nesterov (Nov 04 2022 at 18:41):

Thank you for answers! OK, I will try to complete the matrix group examples for now.

Heinrich Apfelmus (Nov 05 2022 at 14:01):

Hello! :wave: I'm Heinrich and I'm new to Lean. I have a background in mathematics and functional programming (Haskell).

I have a question. Is this a good channel to ask this? If not, where would be more appropriate?

Background: I'm interested in proving statements about functional programs (written in Haskell); think Bird-style proofs. I have had success proving that reverse (reverse xs) = xs for any xs : list α in Lean and now I would like to step up my game by proving statements about abstract data types. In Haskell, we typically build new abstract data types by combining old ones.

Question: I'm constructing an abstract data type, let's call it Foo, by using an abstract data type called Set α (where α : Type) which represents a set of values of type α. I expect that Set will be implemented as an inductive type in terms of binary search trees, with some equivalence relation == representing equality of Set. (I don't understand the distinction between computational and noncomputational well enough to force this to =, I'm happy to live with an equivalence relation on inductive terms.) However, I don't really care how Set is implemented — all I care about are some functions that operate on it and some lemmas about how these functions behave (e.g. a complete axiomatization). In other words, when defining my inductive type Foo, I would like to use the Set α type and functions that operate on it, but I don't want to import an actual implementation — all I care about is a structure that holds a collection of operations and theorems about them, i.e. a "module interface" in programming language speak. How would I go about declaring and using such a module interface (without implementing it)? Should I use type classes?

I have tried constant, but then I run into "noncomputational" issues. I have tried declaring a lot of variable, but that does not give me enough control about their namespace — I would like to write Set.insert x (Set.empty) where e.g. empty : Set α is part of the module interface.

Put differently, I'm writing the abstract data type Foo as follows: "Assume that I have a data type Set α with some lemmas. Then, I define Foo as follows … . Now, from the lemmas about Set, I can prove the following lemmas about Foo: … ". I'm looking for a syntactically nice way of specifying "Assume that I have a data typeSet α".

Johan Commelin (Nov 05 2022 at 14:08):

Welcome! This is certainly the right place to ask your first questions.

Johan Commelin (Nov 05 2022 at 14:08):

I think that you are looking for structure.

Heinrich Apfelmus (Nov 05 2022 at 14:27):

Johan Commelin said:

I think that you are looking for structure.

Maybe. :thinking: Ok, so when I extract the Set interface into a structure, I get the following, which does not work:

structure SetAPI :=
  (Set : Type -> Type)
  (empty : {α}, Set α)
  (insert : {α}, α -> Set α -> Set α)
  (member : {α}, α -> Set α -> bool)
  (prop_insert_member : {α} (x : α) (s : Set α),
    member x (insert x s) = tt
  (prop_insert_comm : {α} (x:α) (y:α) (s : Set α),
    insert x (insert y s) = insert y (insert x s)

variable Set : SetAPI

structure Foo :=
   (bar : Set.Set nat)
   (baz : Set.Set nat)

#check Foo
-- Foo : SetAPI → Type

def insertBar (x : nat) (foo : Foo) : Foo :=
  Foo.mk (Set.insert x (foo.bar)) (foo.baz)

Here SetAPI is a structure that represents the API of the module that I want to import. I define a variable Set in order to "import" it into my namespace. However, this does not quite work as I want it, as Foo gets the type Foo : SetAPI -> Type rather than the type Foo : Type. I understand that this is ultimately correct (the type Foo needs to be supplied with an actual implementation in order to make sense; Foo behaves like a "module functor" in the ML programming language), but for the sake of my own sanity, I would like to have Set : SetAPI as an implicit hypothesis of my entire source file rather than an explicit argument. :thinking: Is there a way to do this?

Johan Commelin (Nov 05 2022 at 14:40):

You can use parameter Set : SetAPI. This is a feature that isn't used so much in the Lean community. But it should do what you want.

Johan Commelin (Nov 05 2022 at 14:40):

It doesn't do exactly the same as in ML modules, but within one file, the behaviour is roughly the same.

Heinrich Apfelmus (Nov 05 2022 at 15:00):

Awesome, thank you! :heart_eyes: Using parameter for assuming a module API works for me at this stage. (I can imagine this becoming unwieldy in larger projects, but I can ask more questions if I get to that point. :grinning: )

Rida Hamadani (Jan 22 2023 at 15:37):

Hi. I think I am starting to understand theorem proving, so I have decided to do my differential calculus homework using lean, and was surprised by how confusing writing a theorem can be. I found an abundance of online guides for theorem proving, but I wasn't able to find a guide on theorem writing. Advice is appreciated, where to start with theorem writing?

Riccardo Brasca (Jan 22 2023 at 15:50):

What is the theorem are you trying to formalize? One problem can be that mathematics in mathlib is probably written in a very general form and you can be confused by this, especially if you are a student and don't know the general formulation used in mathlib.

Rida Hamadani (Jan 22 2023 at 15:56):

As a start, I am trying to prove the following statement:
Given a, b ∈ ℝ, E, F normed vector spaces, T ∈ L(E, F), and f: (a,b) → E differentiable at t, then g = T ∘ f is differentiable at t with g'(t)=T∘ f'(t).

Rida Hamadani (Jan 22 2023 at 16:09):

Here is my code so far:

import analysis.calculus.fderiv
import analysis.normed_space.continuous_linear_map
import linear_algebra.basic

variables {E F : Type*} [normed_add_comm_group E] [normed_space  E]
[normed_add_comm_group F] [normed_space  F] {T : E  F}
{a b : } {t₀ : set.Ioo a b} {f : set.Ioo a b  E}

def g : set.Ioo a b  F := T  f

Attempting to add a [differentiable_at f t₀] after defining f leads to a type mismatch error, is that because its domain is (a, b) ?
Also, I am confused on whether to add given in variables/def fields, or as hypotheses in the lemma .

Riccardo Brasca (Jan 22 2023 at 17:21):

docs#differentiable_at wants 𝕜 as is first variable, not f.

Riccardo Brasca (Jan 22 2023 at 17:22):

But in any case it is not going to work since it is for f : E → F where E is a normed_space 𝕜 E, and set.Ioo a b is not.

Riccardo Brasca (Jan 22 2023 at 17:26):

I suggest to start with f : ℝ → E. If in some application you have a function that is only defined on an interval you can always extend it by 0.

Riccardo Brasca (Jan 22 2023 at 17:27):

But there may be better ways, I am not very familiar with this part of the library.

Riccardo Brasca (Jan 22 2023 at 17:29):

Also, differentiable_at is not a class, so you shouldn't use square brackets. Instead you can write (h : differentiable_at...).

Rida Hamadani (Jan 22 2023 at 17:45):

I see, in that case, I will try to write a differentiable_at that is compatible with intervals, and if that proved to be too difficult, I'll do as you said. Thank you. If someone has other suggestions for this, please share, it would be appreciated.

Riccardo Brasca (Jan 22 2023 at 20:27):

Reinventing the wheel seems a bad idea, especially since you have to build all the API. I am sure it's better to use the already existing library.

Rida Hamadani (Jan 22 2023 at 22:29):

In order to prove the previous statement, I made the following changes:

variables {E F : Type*} [normed_add_comm_group E] [normed_space  E]
[normed_add_comm_group F] [normed_space  F]

lemma lincont_compose_diff_is_diff (T : E   F) (f :   E) (t₀ : )
(f_diff : differentiable_at  f t₀) (T_lincont :  is_bounded_linear_map  T):
differentiable_at  (T  f) t₀  (deriv (Tf) t₀ = T  (deriv f t₀)) :=

However, now I am getting this error message:

  deriv f
has type
  ℝ → E : Type u_1
but is expected to have type
  ?m_1 → ?m_2 → E : Type (max ? ?)

My current understanding is that, while mathematically the composition T∘f has domain ℝ and image E, Lean is interpreting it as T∘f : ℝ → E → F. I would greatly appreciate any assistance in confirming the cause of this problem and finding a solution.

Kevin Buzzard (Jan 22 2023 at 22:32):


Kevin Buzzard (Jan 22 2023 at 22:33):

T ∘ (deriv f t₀) doesn't make any sense, right? That's your problem I think. It doesn't "typecheck".

Rida Hamadani (Jan 22 2023 at 23:03):

f t is in E, implying deriv f t is in E too, and T is from E to F. Why wouldn't it typecheck?

Eric Wieser (Jan 23 2023 at 00:20):

q ∘ p : A → C where p : A → B and q : B → C. You have p as deriv f t : E, which isn't a function

Kevin Buzzard (Jan 23 2023 at 00:59):

\circ eats a function and you gave it a vector

Rida Hamadani (Jan 23 2023 at 07:37):

Oh I see! This is easy to fix, thank you!

Last updated: Dec 20 2023 at 11:08 UTC