Zulip Chat Archive

Stream: Geographic locality

Topic: Dresden, DE


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

view this post on Zulip Johan Commelin (Dec 28 2020 at 15:19):

Welcome! What is the goal of your thesis?

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

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

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

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

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 15:28):

Nice :-)

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

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

view this post on Zulip Yakov Pechersky (Apr 15 2021 at 17:52):

Going to Hell:

Cool stuff!

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

view this post on Zulip Marcus Rossel (Apr 15 2021 at 18:23):

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

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

view this post on Zulip Marcus Rossel (Apr 15 2021 at 18:26):

Oh cool, I didn't know that - thanks

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

view this post on Zulip Jasmin Blanchette (Apr 18 2021 at 06:41):

That takes some courage. ;)


Last updated: May 09 2021 at 22:13 UTC