## Stream: Geographic locality

### Topic: Dresden, DE

#### Marcus Rossel (Dec 28 2020 at 15:04):

Hi there. I'm a CS student at Technische Universität Dresden working on formalizing some maths in Lean for my bachelor's thesis (https://github.com/marcusrossel/bachelors-thesis).

#### Johan Commelin (Dec 28 2020 at 15:19):

Welcome! What is the goal of your thesis?

#### Marcus Rossel (Dec 28 2020 at 15:24):

My supervisor @Andrés Goens has co-published a paper about Reactors : A Deterministic Model for Composable Reactive Systems. I'm trying to formalize a subset of the model in Lean to prove that it is deterministic.

#### Kevin Buzzard (Dec 28 2020 at 15:25):

I love it that in CS people link to some conference proceedings for some international workshop. Where is the free ArXiv link which I can access without having to pay money or log into my work VPN and hope?

#### Kevin Buzzard (Dec 28 2020 at 15:26):

In maths this attitude says "I don't want anyone to read my paper". We don't care where/when it got published, we just want to see the theorems, for free.

#### Marcus Rossel (Dec 28 2020 at 15:27):

Kevin Buzzard said:

I love it that in CS people link to some conference proceedings for some international workshop. Where is the free ArXiv link which I can access without having to pay money or log into my work VPN and hope?

Haha yeah sorry, that link wasn't really useful. I've updated it now.

Nice :-)

#### Kevin Buzzard (Dec 28 2020 at 15:29):

Feel free to ask here if you have any Lean questions; the community can be very helpful and there are certain things which you can only access through it (weird quirks of the system, for example).

#### Marcus Rossel (Apr 15 2021 at 17:43):

The thesis and Lean-formalization can now be found at this link: https://github.com/marcusrossel/bachelors-thesis

Going to Hell:

Cool stuff!

#### Yakov Pechersky (Apr 15 2021 at 18:00):

Is there a reason to define has_equiv expliicitly, instead of making a

def rel := λ r r', r.priorities = r'.priorities ∧ r.reactions = r'.reactions


and proving equivalence rel?

#### Marcus Rossel (Apr 15 2021 at 18:23):

Haha, thanks.
I chose has_equiv for the ≈ notation. Is this kind of perverting has_equiv?

#### Yakov Pechersky (Apr 15 2021 at 18:24):

If you prove equivalence rel then you can make a setoid instance, which gives you a has_equiv instance automatically.

#### Marcus Rossel (Apr 15 2021 at 18:26):

Oh cool, I didn't know that - thanks

#### Kevin Buzzard (Apr 16 2021 at 07:36):

Your slides are really nice -- the way you went through a proof. I'm too lazy to make things line up like that -- I just switch to Lean and do live coding in a lecture.

#### Jasmin Blanchette (Apr 18 2021 at 06:41):

That takes some courage. ;)

Last updated: Jul 29 2021 at 21:10 UTC