00:00:05: Welcome everybody to our latest episode.

00:00:08: So this time we want to go through our second season, Season two and reflect a bit of what happened.

00:00:18: so let's start doing maybe first chronologically for the guests.

00:00:26: I hope Dennis is prepared to say a few words.

00:00:30: Yeah, I mean this was a highlight.

00:00:32: The first of many highlights.

00:00:36: just the very subjective remark is such quick thinker right?

00:00:40: For me sometimes it's hard to follow but here i really took his time.

00:00:45: get things well across and particular insight for my connection with theoretical physics.

00:00:52: maybe logically speaking If category wins the foundational war, then this connection to physics might be a prime reason.

00:01:02: And I think he elaborated nicely how he thinks that this could be the underpinning for new physics.

00:01:10: and so it's

00:01:12: sorry, can we just have an idea?

00:01:17: So if you look back in the history of physics where like Electrodynamic was first understood sort of intuitively, and then the mathematics were developed.

00:01:37: And we had a precise description of electrodynamics.

00:01:41: I think something similar could happen with quantum field theory as an intuitive understanding.

00:01:53: old-fashioned mathematics doesn't seem to be sufficient.

00:01:56: To capture this and people like us use ideas from type theory, to now a homotopy type in particular...to do the mathematic fitting reflecting these intuitive ideas?

00:02:17: No no that's an important point!

00:02:19: And what are your thoughts about Maybe one of the most famous and, uh... One of the foremost successful satirists who was our second guest Joel Hamkins.

00:02:30: Do you think about

00:02:32: it?

00:02:33: I really enjoyed talking to him!

00:02:35: It's like a perfect guest And he had interesting discussions.

00:02:46: This idea of pluralism that there is not, and this I fully sign up to.

00:02:52: That's more than one way to interpret the axioms of set theory.

00:02:57: so it's a multiverse view And maybe i would like talk again.

00:03:06: why stopping at this point?

00:03:08: Why not going further back?

00:03:12: but doesn't that notion of truth itself is problematic.

00:03:18: I mean, to me it seems a bit over... He's the great guy and has absolutely impressive ideas but philosophically for me this is half a house right?

00:03:29: So yeah we have more than one model But its still about tooth.

00:03:35: That seems not fitting.

00:03:46: What do we mean?

00:03:47: I would like to pick up with him.

00:03:54: We should invite him because he hasn't touched the whole corpus of his work, at the end of this episode we talked about infinite time computing and things there that we haven't even touched on.

00:04:05: Let me just add a comment why it's great for you as co-hosts.

00:04:09: For so many philosophers Hamkins is radically too pluralistic And you come here and say, oh that's a way to restrict it.

00:04:17: Why not go for different logics as well?

00:04:21: And also include all of them...

00:04:23: No no!

00:04:23: Not different logicks one different logic.

00:04:29: That is maybe where I always think You don't go the fullway.

00:04:33: But anyway

00:04:37: Okay next was really great Dana Scott agreeing, maybe.

00:04:46: Can you say a few words?

00:04:48: I mean first again it's great honor he did so much for implementing the forcing technique The semantics of Lamna calculus and we wanted also to re-invite him.

00:05:00: but there is one thing where i haven't asked all my question then that V equals L because they are famous theorems famous Scott theorem, showing that you cannot have all large cardinals in the equal L world.

00:05:18: And I think this is like a big reason why only very few mathematicians consider V equals l as good candidate for an extension of ZFC.

00:05:31: and but yeah we should definitely invite him again.

00:05:35: it was great speaking with them And maybe

00:05:38: we should have a premise and you can also explain to me exactly what V because that means.

00:05:43: Yeah, sure.

00:05:43: Also We haven't talked about the other way around why adding choice is like this is not Not a problem for consistency strengths.

00:05:56: I'm very we can talk something and then because of

00:05:59: forcing and related thing.

00:06:03: Yeah, and this is the V-Qual L. Give like a blueprint because

00:06:07: there you can always...

00:06:10: Okay!

00:06:11: And up next another highlight or fourth highlight so far?

00:06:16: Emily Real and what

00:06:18: are

00:06:18: your thoughts on this

00:06:20: episode?

00:06:20: It was great to have Emily on the podcast.

00:06:25: she was very successful.

00:06:26: I mean lots of people watched Emily.

00:06:29: And yeah, this was beautiful and she could explain the idea of or introduce this idea of synthetic mathematics.

00:06:47: She is just a power in doing very... This is really impressive!

00:06:53: She's doing very abstract mathematics But her presentations also and your explanations are very, very clear.

00:07:02: And very understandable.

00:07:03: that's just really beautiful.

00:07:05: Yeah yeah she is a math communicator on top of being world-class mathematician.

00:07:13: in one of these two things it already sufficient for me!

00:07:17: She can do both.

00:07:22: Let me add we haven't talked so much about former verification With.

00:07:28: I mean we had a little bit on it, but there would be something.

00:07:32: We could ask so much more.

00:07:34: She also went really into that.

00:07:36: okay next Werner Schröder and Bernhard Fissenl.

00:07:40: Yeah they're in long time collaborators of mine way.

00:07:44: They Really worked on this approach project with Peter Köpke having an natural input language for theory improving software And I mean its familiar.

00:07:57: Their work is also something where all this AI hype

00:08:01: or

00:08:02: revolution, whatever you want to call it really has an impact.

00:08:06: because they're doing these deep semantics.

00:08:08: Really looking into texts, developing theory understanding deeply and nowadays so much of this simply seemingly falling out off large language models.

00:08:24: but I think as we restrived at the last premises, I think there will be a great synthesis of both.

00:08:32: These deep semantic techniques will greatly benefit from large language models and then vice versa large-language models will benefit from this kind of work.

00:08:42: And another old friend of mine, Jose Perez Escobar has he turned you a Wittgensteinian?

00:08:51: Yeah, I mean he really motivated me to have another look at the late Wittgenstein but i haven't yet had time to dive into this.

00:09:01: I thought it goes in the same direction.

00:09:03: maybe that's your fault as you say is a practice of mathematics.

00:09:09: so Josei is interested why mathematics works And it's very difficult or almost impossible to get him.

00:09:19: on the topic of foundations, which I don't think he is really taking serious.

00:09:24: It's something that you are not interested in... Which i find interesting!

00:09:30: To me seems natural.

00:09:32: if we talk about philosophy and mathematics, I automatically come up with a question for foundations.

00:09:39: but in a way José is much more practical philosopher here.

00:09:48: He says, so why does this actually work?

00:09:50: And he looks in more detail on these things which I find quite fascinating.

00:09:58: So no... and that's very good guest and a very clear presenter so it is pleasant to talk with him.

00:10:09: I mean, this disregard for foundations is something very Wittgensteini and Wittginstein himself disregarded all these developments.

00:10:17: Right?

00:10:17: Yeah right to point to this.

00:10:20: yeah it's true okay yes that's something i learned.

00:10:24: so next one uh is Jan von Plato.

00:10:29: maybe you can say something.

00:10:31: yeah there was.

00:10:32: um i mean i'm not a historian not at all.

00:10:34: so i learnt a lot about the interrelations.

00:10:37: The most surprising thing was that this division of intuitionistic and classical math seems a little bit like a lie in the sense, all the greats at this time did both.

00:10:51: And understood both and compared it to develop both systems.

00:10:57: That's for me the main learning.

00:11:01: I mean he literally wrote so many books about Gürtel that we could have had another four hours and wouldn't fill even one of these.

00:11:11: But you also refuted this idea that Gürtel was a Platonist, right?

00:11:15: That's quite interesting!

00:11:17: Yeah it

00:11:18: seems to be much more complex...

00:11:22: I thought about the strong idea of having a sense organ really feel mathematical truth as being debunked.

00:11:34: It is very an interesting case.

00:11:36: And then the next wave of homotopy type theory arrived

00:11:41: with

00:11:43: Mike, what are your thoughts on this episode?

00:11:49: Yeah.

00:11:51: I mean, he also works together with Emily and here's another example off a really great mathematician who drives so whose subject forward but who's also very good in explaining things.

00:12:08: And what I find all the fascinating and what he himself mentioned is that, we developed some new ideas about type theory so variant of homotopy-type theory.

00:12:26: Mike realized there was no system which supports this style of reasoning.

00:12:36: And so then he sat down and, who is a mathematician?

00:12:40: started to hack his own prof-assistants called Naria as an experiment in still ongoing experiments or that's something somebody has got.

00:12:54: lots needs to be done, he will just do it.

00:13:01: He's very brave in a way.

00:13:02: I mean i would have not touched this idea of now implementing new proof assistant To realize these ideas and start doing that himself.

00:13:15: That was...I mean..he is working together with some other people but thats very impressive Is Tudor right?

00:13:33: Yeah, exactly.

00:13:36: I mean let me say something that sounds maybe a little unfair There.

00:13:41: this was the episode where iIwasthemostscared because i thought oh Maybe there's somebody just trying to sell saying Oh This is so great!

00:13:50: This will solve everything!Thisisjustperfect butiwaspleasantlysurprisedthat he seemedtobevery aware of the minute details that play your role, like bugs training data.

00:14:09: We will stick to this topic a little bit just because it's simply so impactful right now.

00:14:15: The synthesis of lean and large language models allowing these tools to reiterate ideas something that works so astonishingly well.

00:14:30: and a while ago it was only, oh they only win gold medals in Martha Olympiad then.

00:14:37: It was Oh this is only like one annual paper now its only one of the millennium problems.

00:14:44: maybe it's already two.

00:14:46: when this episode premieres um... And it raises so many questions for the mathematical community.

00:14:56: look forward to find a good discussion of these, because it's also... Because its'a political theme.

00:15:05: It is often either so overhyped or so doom-resistic that the word.

00:15:14: but I think his discussion was very fair and in the middle really understood both sides.

00:15:21: What i found interesting he discovered Lean because they didn't start with saying, okay we now try to prove some lean theorems.

00:15:31: They started by saying Okay We want have a system which creates mathematical proofs and mathematical proof is just I think initially wanted us create text basically in English texts but then realized that there was no way to certify this actually approve.

00:15:51: And that's when they started using Lean.

00:15:54: That is exactly my thesis, it was a combination of statistic AI and symbolic AI as actually marriage made in heaven right?

00:16:04: They discovered this!

00:16:05: It wasn't their starting point.

00:16:08: I'm willing to

00:16:10: know... No thats interesting.

00:16:11: also maybe brings us our final guess for the season.

00:16:16: but more than AI gets more complex.

00:16:21: they had their tool, but Neil has his own ideas how to navigate the time of Agentec AI.

00:16:30: What do you thought about our final episode of season two?

00:16:34: Yeah so I mean Neil is an old friend and collaborator with mine.

00:16:39: So naturally it was a bit maybe more critical than usual completely sold to the idea that you want to build in symbolic structures based on category theory, based on types.

00:17:05: In your statistic.

00:17:07: maybe I should be in favor because it's a good way maybe to get money from whatever.

00:17:13: But I think these structures should emerge and shouldn't be put in form.

00:17:24: the beginning, that's for something where wasn't completely convinced.

00:17:29: but it is certainly interesting what Neal was doing very exciting his views on how agentic AI can be improved using ideas from categorical theory, type theory.

00:17:47: And so if this works out but I'm still a bit skeptical?

00:17:52: I mean maybe me being a friend of yours i need to be critical of your thoughts and it was quite sold because i just think the immediate safety ramifications are simply huge.

00:18:09: There is this point of if we treat everything on the same level, and I mean you should be critical off set theory.

00:18:17: That's what we do in set theory.

00:18:19: then You can have these weird arrows with weird things free an element of seven.

00:18:26: And all this happens in large language models because system problems inputs.

00:18:33: Everything just text.

00:18:34: text goes in text goes out.

00:18:37: And I mean, this is no.

00:18:39: website should not sanitize user input in the slash language world.

00:18:45: It's all just text and of course oversimplifying.

00:18:48: No-no i'm not saying that you do need structure on that.

00:18:52: You don't need types obviously are not saying This?

00:18:54: I am Just saying maybe it something which Should emerge instead Of being built into That.

00:19:00: And maybe that's consistent with what Neil is thinking, so I don't want to put anything in his mouth.

00:19:09: Great and then there was another big sub-series starting the premises... Before

00:19:17: we do this can you because i talk and it came up with some structure, I mean some emergent structure for our second season.

00:19:35: It didn't get completely right.

00:19:36: so this is quite interesting.

00:19:38: when you say yeah maybe i'm asking something or suggest something then like saying no-no-no that's not the right way to discuss going.

00:19:46: So one thing about topics which come.

00:19:51: So one is so foundations in philosophy, which I mean a very important topic.

00:19:57: And you could say Hamkins, Scott and von Plato fit into this right?

00:20:03: Where as Scott and from Plato may be more the historic aspect on Hamkin's sort of modern foundation or philosophy.

00:20:15: Then another topic that was not surprising is type theory and higher mathematics.

00:20:22: What do we mean by higher mathematics?

00:20:24: Higher, I mean in the sense of infinity categories or infinity group rates.

00:20:30: where you have this structure of equality it's not trivial.

00:20:38: maybe should make a premise on that because i think there are very important insight.

00:20:43: what does he means by high mathematics or Schreiber, Emily Riel and Mike Schulmann who really covered this very nicely.

00:20:57: Next topic is language and mathematical practice?

00:21:02: Yeah I mean it's

00:21:02: a topic close to your heart.

00:21:06: We had that in season one and in Season two probably Rosse and Sanyi and Schröder.

00:21:14: they mathematical practice, I mean because it's still humans doing.

00:21:19: The AI hasn't fully taken over and that won't.

00:21:23: but there is a lot going on in mathematical departments that often overlooked.

00:21:29: if you have your abstracted view of math just producing theorems and exchanging certificates for those theorems much more happening, definitions are created.

00:21:43: There even epistemic considerations what's nice?

00:21:48: What a fashion and all these points.

00:21:55: And finally AI in the future of mathematics.

00:21:59: I mean you could say Future of Mathematics is maybe real shulman but the AI aspect And I'm sure we will cover more of this topic in future.

00:22:13: Yeah,

00:22:14: and i guess we want to keep all three strengths going right?

00:22:18: It's nothing gets outdated or relevant but it all affects each other at the same time...

00:22:26: ...I had four!

00:22:28: Four?!

00:22:28: Oh which is your fourth one?

00:22:29: who have forgotten...?

00:22:30: Foundation philosophy, type theory higher mathematics.

00:22:35: second third one language mathematical proxies and then AI in future of mathematics.

00:22:41: Okay, I just miscounted.

00:22:43: it's not so easy at all you know?

00:22:44: Yeah.

00:22:45: Just finite ordinals who cares less than omega great um And do want

00:22:54: to say something about premises?

00:22:56: no

00:22:56: yeah exactly.

00:22:57: and i think It's necessary because first Of All I'm very surprised how good this works because in some sense, of course we aren't doing mathematical research.

00:23:10: In real time.

00:23:11: that's nothing we do.

00:23:13: but it's also not basic communications and I think some of the guests are really going quite advanced saying a few things here or there where even i cannot follow... Where some notions were introduced without much introduction Because they live in this world right?

00:23:33: They did every day And I think there is value in that, because it's not repeating the narratives.

00:23:41: Not repeating the advertisements how one often talks about a field but really talking about your own experience and practice.

00:23:51: But if you have this approach You also need to give some background.

00:23:55: We try do that in the premises.

00:23:58: we went into set theory for instance having an introduction there, we explained what synthetic mathematics really is in the whole episode.

00:24:07: We focus on particular gold nuggets like this...

00:24:13: Axial of choice!

00:24:15: Yeah exactly This was that

00:24:17: episode.

00:24:18: Let's go who.

00:24:19: I turned into Georgian even though he Obviously Romanian, that was embarrassing.

00:24:27: But the good thing is this shows how good our comment section is and we're impressed there right?

00:24:35: I'm always very happy to have Andre there whenever i see some fast guests or friends in.

00:24:42: it's particularly interesting And so many repeated offenders commenting on most episodes and so many pointers to the literature, other relevant aspects.

00:24:57: We nurture a little but growing community of people with an interest in all four themes that we mentioned.

00:25:09: Anything you would like to add on the premises?

00:25:11: Yeah I'd like Questions, what we should or making proposals.

00:25:20: What you should cover in premises?

00:25:23: I think i mentioned already something.

00:25:25: maybe it's about higher mathematics and another question is whether we should include some lectures using whiteboards which obviously doesn't work for the podcast system But we could still add it as an additional resource, so I wonder if there's any interest in doing this.

00:25:49: As a sideline tutorials or whatever to cover some background?

00:25:59: No that is the great idea of having introduction into type theory.

00:26:04: maybe just have a great lecture over

00:26:08: here Joe, to give us an introduction to a set theory.

00:26:13: that would be also cool.

00:26:15: Yeah sure it'd be lovely.

00:26:18: Okay great um.

00:26:19: having said that let's look into the future.

00:26:22: what will season three bring?

00:26:23: or will there even be season three?

00:26:26: Yes yes start this

00:26:29: already.

00:26:29: yeah kind of um.

00:26:31: here we are recording right now.

00:26:34: The first guests are already fixed, but we will keep it a secret.

00:26:38: But there's also still wiggle room.

00:26:40: so... We're happy about suggestions and of course not honor every suggestion because many people here sometimes don't join us in the podcast with no shaming as always voluntarily.

00:26:58: Having said that I think only left to say thank you once!

00:27:03: And

00:27:04: thank you for all the support and also useful feedback.

00:27:15: Thank.