Zulip Chat Archive

@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?

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?

Simon Hudon (Sep 09 2019 at 00:22):

Where do we want to go?

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.

Simon Hudon (Sep 09 2019 at 00:37):

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

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.

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.

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.

Floris van Doorn (Sep 09 2019 at 00:57):

at 7pm?

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

Rob Lewis (Sep 09 2019 at 01:08):

7pm at the Vietnamese place? Works for me.

Rob Lewis (Sep 09 2019 at 01:08):

It will be like a Hanoi reunion.

Floris van Doorn (Sep 09 2019 at 01:14):

Yeah :)

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.)

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

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?

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 :-)

Kevin Buzzard (Sep 09 2019 at 21:16):

Maybe they're all just privately angry.

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.)

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.

Rob Lewis (Oct 01 2019 at 09:08):

I think Mario recorded himself.

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

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.

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.)

Johan Commelin (Oct 02 2019 at 09:10):

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

Wojciech Nawrocki (Oct 02 2019 at 17:30):

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

Wojciech Nawrocki (Oct 08 2019 at 00:07):

Maybe also this @Mario Carneiro

Last updated: Dec 20 2023 at 11:08 UTC