# Zulip Chat Archive

## Stream: Geographic locality

### Topic: Zurich, CH

#### Tobias Grosser (Apr 12 2020 at 13:14):

Working from home. Stay safe everybody!

#### Ödül Tetik (Oct 04 2021 at 09:40):

Next semester (starting February 2022), we'll organise an informal seminar (one doesn't give credits) on Lean in Zurich, with a booked room and announcements on uni websites and everything. If you're interested, you're most welcome to already let me know, here or via email (find me on the UZH website) or both.

I myself work in mathematical physics (mostly around algebra and topology), and the coorganiser works in applied algebra. So it's going to be a diverse group of people :)

#### Ödül Tetik (Oct 04 2021 at 09:43):

Any suggestions on what to cover given the time constraints? We're still learning ourselves, of course :)

#### Oliver Nash (Oct 04 2021 at 09:46):

Sounds exciting! IMHO, this might be worth cross-posting in #general to get better visibility.

#### Alex J. Best (Oct 04 2021 at 10:56):

If the goal is to learn to use lean as a bunch of curious mathematicians then maybe you could try to follow the material from the Lean for the curious mathematician workshop in 2020 https://leanprover-community.github.io/lftcm2020/schedule.html most of these sessions were in the format of a short introductory tutorial to an area (which are now on youtube https://www.youtube.com/playlist?list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N) and then some Lean based exercises which really try to teach the material by doing. Maybe looking at one session per week would work, depending on how long the seminar is, and you can all talk over the exercises together or something like that.

#### Kevin Buzzard (Oct 04 2021 at 11:06):

Here is the material which I used with PhD students (mathematicians, but no Lean experience). In January I will be running a similar course but for undergraduates.

#### Ödül Tetik (Oct 04 2021 at 15:03):

Wow, I wasn't aware of these, thanks!!

#### Johan Commelin (Oct 08 2021 at 09:19):

@Ödül Tetik I'd be interested in receiving announcements. (I'm in Freiburg, just across the border in Germany.)

#### Elif Sacikara (Alumni) (Nov 03 2021 at 22:14):

Hello,

When we (with Ödül and some colleagues from the Institute) tried to prove that any function from a discrete topological space to any other topological space is continuous, as we attempted to state it in Thm discrete_left_adj_forget by the code below, we have seen the corresponding info view in Lean, respectively.

Lean code:

def continuous {X Y : Type} (X_top : topological_space X) (Y_top : topological_space Y) (f : X → Y)/-can not we introduce them as variables like in Sec 2.6.-/ : Prop :=

∀ (U : set Y), (Y_top.is_open U) → (X_top.is_open (preimage f U))

def top_discrete (X : Type) : topological_space X := topological_space.mk

(λ (S : set X), true)

(trivial)

(begin

intros H1 H2 H3 H4,

trivial,

end)

(begin

intros H1 H2,

trivial,

end)

theorem discrete_left_adjoint_forget {X : Type} : ∀ {Y : Type}

(Y_top : topological_space Y) (f : X → Y), continuous (top_discrete X) Y_top f :=

begin

intros Y Y_top f,

intros U,

end

Lean infoview:

XY: Type

Y_top: topological_space Y

f: X → Y

U: set Y

U_open: Y_top.is_open U

⊢ (top_discrete X).is_open (f ⁻¹' U)

We would like to evaluate this function (top_discrete X).is_open (preimage f U) to be `true’’ in Lean infoview, since in `

top_discrete’’ we defined this function using the lambda expression which turns out to be `True". When we #reduce (top_discrete X).is_open (preimage f U) outside of the tactics mode, then it evaluates it as being `

true". So even though it can do it outside of tactics mode, this is not the case inside of the proof and now we are trying to find a way to make lean show that this expression is as true inside of proof. Thanks in advance.

#### Kevin Buzzard (Nov 03 2021 at 22:21):

#### Kevin Buzzard (Nov 03 2021 at 22:21):

and probably you want to ask this in #new members rather than here -- many more people will see it over there

#### Elif Sacikara (Alumni) (Nov 03 2021 at 22:22):

Thanks so much for the remark! I am posting there now.

#### Elif Sacikara (Alumni) (Feb 20 2022 at 14:16):

Hello Everyone,

As @Ödül Tetik mentioned before, starting from 25.02.2022, we will be organizing an informal seminar which will be held on Fridays between 13:00-15:00 at the Institute of Mathematics, UZH (Campus Irchel, Y27H12). You may find general information on the seminar website: https://sites.google.com/view/uzh-lean-seminar/home.

#### Ödül Tetik (Feb 24 2022 at 20:33):

@Kevin Buzzard many thanks for advertising our seminar on Twitter!

#### Kevin Buzzard (Feb 24 2022 at 23:35):

No problem!

#### Elif Sacikara (Alumni) (Feb 26 2022 at 18:28):

Elif Sacikara (Alumni) said:

Hello Everyone,

As Ödül Tetik mentioned before, starting from 25.02.2022, we will be organizing an informal seminar which will be held on Fridays between 13:00-15:00 at the Institute of Mathematics, UZH (Campus Irchel, Y27H12). You may find general information on the seminar website: https://sites.google.com/view/uzh-lean-seminar/home.

Even though each time I appreciate the difficulty of challenging works, giving an introduction talk about Lean was at another level. You may find the slides of the first meeting here. Thanks for all open resources that are quite helpful and apologies if there is something wrong with the information we presented.

Last updated: Oct 06 2022 at 05:33 UTC