The Netherlands

Stream: Geographic locality

[Marco Vasquez Beltran]

Hello everybody

[Kevin Buzzard]

You might want to post that comment in the relevant thread rather than the San Francisco one...

[Marco Vasquez Beltran]

Kevin Buzzard said:

You might want to post that comment in the relevant thread rather than the San Francisco one...

Thanks for the clarification, just noticed :+1:

[Anne Baanen]

Hello! I'm also in the Netherlands :D

[Anne Baanen]

Can I ask where you are located? I'm in the finishing stage of my PhD at the VU in Amsterdam.

[Marco Vasquez Beltran]

Oh, nice to meet you. I am post-doc in Eindhoven

[Johan Commelin]

Cool, whose group are you in? (I'm in Utrecht.)

[Marco Vasquez Beltran]

DSC

[Johan Commelin]

Sorry, I don't recognise that acronym

[Marco Vasquez Beltran]

Dynamical Systems and Control

[Johan Commelin]

@Marco Vasquez Beltran Are you planning to formalize some stuff about dynamical systems in Lean?

[Johan Commelin]

Btw, Jim Portegies and Jelle Wemmenhove are also using proof assistants in Eindhoven.

[Andrés Goens]

I'm also in Amsterdam (well, at least I will be from Monday on), at UvA!

[Shreyas Srinivas]

Does this include formalization of discrete linear recurrences? I am guessing not, but it would be nice to try. There are a bunch of recent results about decidability of the zero and orbit problems

[Marco Vasquez Beltran]

@Johan Commelin I am not sure, I am just starting to learn it. In which group are you?

[Johan Commelin]

I'm in the logic group in Utrecht, but I also hang out with the number theorists, algebraic geometers, and the PL group in computer science.