Zurich, CH

Stream: Geographic locality

[Tobias Grosser]

Working from home. Stay safe everybody!

[Ödül Tetik]

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]

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

[Oliver Nash]

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

[Alex J. Best]

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]

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]

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

[Johan Commelin]

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

[Elif Sacikara (Alumni)]

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]

#backticks

[Kevin Buzzard]

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

[Elif Sacikara (Alumni)]

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

[Elif Sacikara (Alumni)]

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]

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

[Kevin Buzzard]

No problem!

[Elif Sacikara (Alumni)]

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.

[Moritz Firsching]

I work in Zurich, always happy to chat about lean

[David Loeffler]

Hi folks,

I'd like to advertise two forthcoming Lean-related events in Zurich:

• Firstly, @Kevin Buzzard will be giving the Paul Bernays Lectures at ETH on August 28th-30th, on "Mathematics and the computer". The course will consist of 3 lectures, "Can AI do mathematics?", "What is an interactive theorem prover?", and "The Liquid Tensor Experiment". For more details see https://math.ethz.ch/news-and-events/events/lecture-series/paul-bernays-lectures/bernays-2023.html.

• Secondly: I'll be organising a student seminar at ETH this autumn on "Formal theorem-proving with Lean". This is primarily aimed at ETH bachelor / master students but there should be room for a few guests. More details to follow.

[Luis Wirth]

Hi everyone!
My name is Luis Wirth. I'm a 3rd-year bachelor student in CSE at ETH. I've recently discovered lean and started learning it on my own. I am really enjoying learning lean as a new (very extraordinary) programming language and whilst doing so also learning about formal logic and theorem proving. I'm considering Lean as a potential focus for my bachelor's thesis, but this has yet to become concrete. I'm actively seeking advice on finding a suitable supervisor and would appreciate any pointers on how I should approach writing a thesis involving lean in general.

[Luis Wirth]

And if there's somebody at ETH or in Zurich who wants to chat about lean, I would gladly do so :)

[Tobias Grosser]

I am in Zurich beginning next week and would be happy to have a brief chat.