Dresden, DE

Stream: Geographic locality

[Marcus Rossel]

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]

Welcome! What is the goal of your thesis?

[Marcus Rossel]

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]

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]

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]

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.

[Kevin Buzzard]

Nice :-)

[Kevin Buzzard]

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]

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

[Yakov Pechersky]

Going to Hell:

Cool stuff!

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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

[Marcus Rossel]

Oh cool, I didn't know that - thanks

[Kevin Buzzard]

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]

That takes some courage. ;)