Zulip Chat Archive

Stream: general

Topic: ITP 2019


view this post on Zulip Rob Lewis (Sep 06 2019 at 17:28):

Hey, who's going to be in Portland this week for ITP? I'm getting in tonight.

view this post on Zulip Rob Lewis (Sep 06 2019 at 17:28):

@Floris van Doorn and @Kevin Buzzard I know. @Mario Carneiro @Simon Hudon @Jesse Michael Han @Minchao Wu @Cyril Cohen ?

view this post on Zulip Simon Hudon (Sep 06 2019 at 17:29):

I am!

view this post on Zulip Jesse Michael Han (Sep 06 2019 at 17:34):

i arrive sunday afternoon

view this post on Zulip Simon Hudon (Sep 06 2019 at 17:35):

Saturday evening

view this post on Zulip Floris van Doorn (Sep 06 2019 at 17:36):

I'm also arriving Saturday evening.

view this post on Zulip Johan Commelin (Sep 06 2019 at 17:36):

I can't come: https://cplx.vm.uni-freiburg.de/omin/

view this post on Zulip Jesse Michael Han (Sep 06 2019 at 17:38):

that looks fun though!

view this post on Zulip Johan Commelin (Sep 06 2019 at 17:53):

Too bad Lean can't attend my workshop (-;

view this post on Zulip Johan Commelin (Sep 06 2019 at 17:53):

Lean mathlib still doesn't know what a scheme is.

view this post on Zulip Mario Carneiro (Sep 06 2019 at 19:16):

I am arriving Sunday noon

view this post on Zulip Patrick Massot (Sep 06 2019 at 20:28):

I like the picture of summer in Freiburg on top of the webpage

view this post on Zulip Kevin Buzzard (Sep 06 2019 at 21:21):

I will get there on Sunday afternoon

view this post on Zulip Minchao Wu (Sep 06 2019 at 22:00):

I'm arriving tonight, too, but will probably spend the weekend in Seattle, and get back on Sunday afternoon

view this post on Zulip Jeremy Avigad (Sep 07 2019 at 20:45):

@Johan Commelin The summer school looks great. It is nice to see o-minimality make it into the mathematical mainstream. Will the lectures be recorded?

view this post on Zulip Floris van Doorn (Sep 09 2019 at 00:04):

To people who already arrived in Portland: is anyone interested in going out for dinner tonight?

view this post on Zulip Simon Hudon (Sep 09 2019 at 00:22):

Where do we want to go?

view this post on Zulip Floris van Doorn (Sep 09 2019 at 00:36):

The thought was to go a bit north of the conference center, where there are more options.

How about Luc Lac Vietnamese Kitchen?
I'm also fine with meeting anywhere, and then deciding where to go.

view this post on Zulip Simon Hudon (Sep 09 2019 at 00:37):

That works too. I'm at the workshop. It just ended. Where are you?

view this post on Zulip Floris van Doorn (Sep 09 2019 at 00:39):

I'm in my hotel (5 minutes walking away). I could come over now, but I think Rob wanted to have dinner a bit later.

view this post on Zulip Rob Lewis (Sep 09 2019 at 00:55):

That works for me! If anyone's interested in checking out a brewery there are tons of them right across the river (e.g. https://www.rogue.com/meeting-halls/rogue-eastside-pub-pilot-brewery) all with plenty of food options. But it's a bit more of a trip and the brewery part might not be a draw for everyone.

view this post on Zulip Rob Lewis (Sep 09 2019 at 00:55):

Any time is fine with me. I'm staying a 15-20 minute walk north of the conference.

view this post on Zulip Floris van Doorn (Sep 09 2019 at 00:57):

at 7pm?

view this post on Zulip Simon Hudon (Sep 09 2019 at 01:07):

Actually, I think I’m going to take a rain check. I need to work on my slides

view this post on Zulip Rob Lewis (Sep 09 2019 at 01:08):

7pm at the Vietnamese place? Works for me.

view this post on Zulip Rob Lewis (Sep 09 2019 at 01:08):

It will be like a Hanoi reunion.

view this post on Zulip Floris van Doorn (Sep 09 2019 at 01:14):

Yeah :)

view this post on Zulip Johan Commelin (Sep 09 2019 at 04:16):

Johan Commelin The summer school looks great. It is nice to see o-minimality make it into the mathematical mainstream. Will the lectures be recorded?

@Jeremy Avigad If any recordings are made, I'll let you know. (I didn't organise that part.)

view this post on Zulip Kevin Buzzard (Sep 09 2019 at 17:44):

My talk was not videoed but here are the notes: wwwf.imperial.ac.uk/~buzzard/one_off_lectures/itp.pdf

view this post on Zulip Jeremy Avigad (Sep 09 2019 at 20:19):

Nice! How was the talk received? Did the audience stand and cheer or did they throw rotten tomatoes? How did the other Lean talks go?

view this post on Zulip Kevin Buzzard (Sep 09 2019 at 21:16):

So far we've had Mario on computability and Jesse with his+Floris work on CH. There were no rotten tomatoes in my talk, and indeed I didn't even seem to make anyone angry despite suggesting that all of their work in mathematics was concentrating on the wrong area :-)

view this post on Zulip Kevin Buzzard (Sep 09 2019 at 21:16):

Maybe they're all just privately angry.

view this post on Zulip Mario Carneiro (Oct 01 2019 at 08:43):

My friday ITP talk about MM0 and x86 is now on youtube: https://youtu.be/7hAShC6K_vA . (Unfortunately the recording of my Monday talk, about computability theory in lean, was eaten by a bad backup tool, but the slides are available at https://itp19.cecs.pdx.edu/wp-content/uploads/2019/09/carneiro_slides.pdf.)

view this post on Zulip Kevin Buzzard (Oct 01 2019 at 09:07):

They didn't video most of the talks, right? Was Friday special? I don't understand this claim about your Monday talk. Did someone video it? Did they video my talk too? I thought nothing was videoed Mon-Thu.

view this post on Zulip Rob Lewis (Oct 01 2019 at 09:08):

I think Mario recorded himself.

view this post on Zulip Mario Carneiro (Oct 01 2019 at 09:14):

When I tried to get the monday talk off my phone, the connection was interrupted and I lost both copies. I spent several hours trying to root my phone so I could recover it before finding out that samsung has good security and doesn't like its users to have root access

view this post on Zulip Floris van Doorn (Oct 02 2019 at 02:21):

Thanks for posting Mario! I was sad to miss your talk.

I like how two main points of your talk are:

  • Don't try to formalize anything that wasn't designed to be formalized
  • Let's formalize x86

I understand how you got from the former to the latter, but it's pretty self-contradictory.

view this post on Zulip Mario Carneiro (Oct 02 2019 at 04:59):

The tempering note there is that you have to stay tethered to reality. In a perfect world, we formalizers would also be able to modify the hardware to suit our purposes, and then we could eliminate that "bad day" by making something more formalization friendly. But sometimes you just have to work with an unyielding interface. (The math analogue would be that in flypitch, while you can change internal statements as you like, the final result should actually be about CH and should actually be about ZFC, where these things are defined elsewhere by community convention and you don't have permission to change them. The name of the game then becomes abstracting away from that hard reality as soon as possible until you get the needed flexibility.)

view this post on Zulip Johan Commelin (Oct 02 2019 at 09:10):

@Mario Carneiro That was a nice talk to watch. Thanks for sharing the recording.

view this post on Zulip Wojciech Nawrocki (Oct 02 2019 at 17:30):

@Mario Carneiro I'd say this blogpost is relevant :)

view this post on Zulip Wojciech Nawrocki (Oct 08 2019 at 00:07):

Maybe also this @Mario Carneiro


Last updated: May 08 2021 at 09:11 UTC