Dagstuhl

Stream: general

[Patrick Massot]

So, how is the Dagstuhl meeting going on?

[Mario Carneiro]

The lean group here includes me, Johannes, Floris and Scott Morrison

[Patrick Massot]

Great team! What are you up to?

[Scott Morrison]

My Dagstuhl demo is online at <https://www.youtube.com/watch?v=U_22O1O9nGc>.

[Johannes Hölzl]

People were quiet impressed by the graph visualization. And also by the short formalization of Yoneda itself :-)

[Johan Commelin]

Awesome! Well done Scott!

[Patrick Massot]

Indeed it was very impressive and fun to watch.

[Kevin Buzzard]

What does Scott say at around 1 minute 50 -- his goal was "to be able to report back to my collegues in the math department about whether it's time something something something theorem provers"?

[Chris Hughes]

I think it's "they should start paying attention to interactive theroem provers"

[Patrick Massot]

Thanks Kevin. I planned to spend all week-end listening to this video to get used to Scott's accent before he comes to Orsay. But maybe I don't need to if you also struggled.

[Kevin Buzzard]

It was more the fact that Scott was quite a way from his laptop mic when he said it :-) I guess I agree with him that there's no point telling the staff to pay attention, that's why I'm telling the students.

[Patrick Massot]

I also noticed that it got easier when listening on my computer instead of my phone with crappy internet.

[Sean Leather]

@Scott Morrison: You must have impressed the right people (in Germany no less!) if you're about to become the next prime minister of Australia.

[Kevin Buzzard]

Indeed I'm slightly worried about whether he'll make it to Paris next week...

[Scott Morrison]

Okay --- one more report from Dagstuhl, as formal abstracts is being discussed after @Floris van Doorn's presentation.

[Scott Morrison]

After someone asked whether results will be tagged as to whether or not they were constructive, I had to bite my tongue to avoid saying this this meeting was the first time I had met in person someone with a job in a mathematics department who did constructive mathematics.

[Scott Morrison]

(That would have been a slight lie; I think it's the second time.)

[Kevin Buzzard]

My impression is that computer scientists have a largely incorrect view about how much constructive mathematics goes on within a mathematics department. My impression is that most people that work in maths departments would have real trouble even stating what it means for a result to be constructive and giving basic examples of mathematics which is or is not constructive. If people in maths departments are doing constructive mathematics, my gut feeling is that they are doing it by accident.

[Sean Leather]

@Kevin Buzzard: Do logicians count in the set of people working in mathematics departments?

• https://www.math.su.se/english/research/2.19150/logic-group/logic-group-1.70775
• http://www.maths.manchester.ac.uk/our-research/research-groups/mathematical-logic/
• https://math.nd.edu/research/research-groups-in-mathematics/logic/
• http://logic.berkeley.edu/
• http://www.math.wisc.edu/~lempp/main.html#other

[Scott Morrison]

Sure! I think they count. Kevin is wrong in the sense that most logicians can explain what constructive mathematics is. But I don't recall talking to any logicians who actually did it.

[Kevin Buzzard]

The number of logicians in most maths departments in the UK is 0

[Kevin Buzzard]

At my university it was 0 for over 20 years but we just hired two recently.

[Kevin Buzzard]

as to whether they count -- sure they count, if they're working in a maths department. But perhaps it's also worth noting that even within the maths departments I've worked in, the logicians feel like a separate group to the rest of the researchers; Berkeley was a great example, where the logicians occupied a different floor to the other pure mathematicians and I think that in my 2 years there I didn't ever bump into any. On the other hand I had plenty of mathematical interactions with geometers, topologists and algebraists when I was there (I'm a number theorist). I very much felt with the logicians that it was a case of "they don't know anything about what we do, and we don't really care what they're doing, for the most part". Logicians have always felt very much like the outsiders in mathematics departments I've worked in. Of course this is just my personal impression.

[Patrick Massot]

Scott Morrison: You must have impressed the right people (in Germany no less!) if you're about to become the next prime minister of Australia.

It seems hiding in the most remote place at the other end of the world was a good strategy: all his colleagues fought among themselves, and Scott was the last one standing (at least this how it looks like in French newspapers).

[Scott Morrison]

It's true the only maths department I've been in with logicians was Berkeley. There I had some contact with them, but solely with the graduate students, essentially through the non-mathematical social life of the department.

[Sean Leather]

This has all been very enlightening. I'm rather ignorant of what goes on in mathematics departments. This wasn't something we covered in any of my computer engineering, electrical engineering, or computer science courses or research.

My impression is that computer scientists have a largely incorrect view about how much constructive mathematics goes on within a mathematics department.

My personal experience suggests that this is largely overstating the views of computer scientists. I'd guess that most of them actually do not know or care much about constructivism or whether it is used by mathematicians. It's a rather small group of computer scientists who actually use it in research, and they're vastly outnumbered by computer scientists working in other areas.

[Kevin Buzzard]

The research that goes on in maths departments (in the UK at least) is 99% classical logic being used to study what we call algebra, number theory, geometry, topology, analysis (and in the UK maybe some combinatorics), although these are pretty broad terms and what they mean changes all the time. Most of the people doing this have no idea what the law of the excluded middle or constructive maths is. You're right that the computer scientists I'm talking about are the ones I've met here though, which I'm sure is not at all a representative sample. Moreover, these mathematicians I'm talking about for the most part have no idea that things like Coq exist, either that or they do know but don't care.

[Johan Commelin]

Did anyone give Neil Strickland a pointer to Zulip?

[Kevin Buzzard]

"You are absolutely welcome to come and hang out with us any time at the Zulip chat. We're going to have perfectoid spaces soon". From my sent-mail.