Zulip Chat Archive

Stream: Geographic locality

Topic: Zurich, CH


view this post on Zulip Tobias Grosser (Apr 12 2020 at 13:14):

Working from home. Stay safe everybody!

view this post on Zulip Ö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 :)

view this post on Zulip Ö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 :)

view this post on Zulip Oliver Nash (Oct 04 2021 at 09:46):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ödül Tetik (Oct 04 2021 at 15:03):

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

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 03 2021 at 22:21):

#backticks

view this post on Zulip 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

view this post on Zulip Elif Sacikara (Alumni) (Nov 03 2021 at 22:22):

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

view this post on Zulip 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.

view this post on Zulip Ödül Tetik (Feb 24 2022 at 20:33):

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

view this post on Zulip Kevin Buzzard (Feb 24 2022 at 23:35):

No problem!

view this post on Zulip 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