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):

#backticks

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.

Moritz Firsching (Nov 25 2022 at 09:56):

I work in Zurich, always happy to chat about lean

David Loeffler (Aug 12 2023 at 07:46):

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 (Nov 11 2023 at 02:39):

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 (Nov 13 2023 at 09:54):

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

Tobias Grosser (Nov 13 2023 at 10:20):

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


Last updated: Dec 20 2023 at 11:08 UTC