aboutlogic #15 | Emily Riehl – Higher Category Theory, Homotopy & AI in Math

00:00:00: I guess maybe i have a question for you.

00:00:02: There's something that im curious about which seems to be historical or practical, circumstantial split between the type theory community and set-theory logic community.

00:00:22: Hello!

00:00:22: Im very happy today to have Emily Rieu with us.

00:00:26: She is professor of mathematics at Johns Hopkins University And I've met her several times and always enjoy talking to her or listening to her talks.

00:00:37: She's an expert in higher category theory, right?

00:00:40: Is it fair to say how would you describe yourself

00:00:44: Emily?

00:00:44: Sure yeah that sounds great

00:00:47: okay so i just looked up.

00:00:50: apparently was Stenrod who said categories here is abstract nonsense.

00:00:55: So are doing higher abstract non-sense?

00:00:59: Sure, increasingly abstract nonsense perhaps.

00:01:03: I love that quote of Steenrod and he meant it positively.

00:01:06: so sometimes people... Abstract non-sense is kind of like queer in different things when using that but its been embraced by the Category Theory community for a certain style of proof.

00:01:20: those who are working on Category theory really liked what drew me to this field.

00:01:26: But you didn't get stuck there with category theory?

00:01:29: You went for the full Monty, higher stuff.

00:01:34: Well I think so.

00:01:35: initially first became interested in Category Theory and a year i spent at Cambridge took of course by Peter Johnstone an eight week maybe ten week, I forget how long the terms are there.

00:01:50: Of course in category theory that covered quite a lot of material and short amount of time...I sort of took the year to kind of fully absorb the course And then starting that summer i attended my first international Category Theory conference which really gave me a sense And I found myself drawn to talks that involved abstract homotopy theory in some way.

00:02:15: So, some categorical abstractions you know such as due to Quillen?

00:02:19: That allows you to kind of mimic constructions from Homotopy Theory and more general categories...and now that is understood as being sort presentation a higher dimensional structure on the category.

00:02:33: so i guess thats how got into Higher Category Theory.

00:02:36: Maybe you can say a few words about homotopic theory and what it is in your adventures.

00:02:41: Sure, right.

00:02:43: so there's this fundamental mathematical question maybe philosophical question of when is one thing the same as another?

00:02:51: And There are different ways that You Can answer It!

00:02:54: There's sort Of The Answer Embedded In First Order Logic.

00:02:58: This Is Leibniz' in discernibility of identicles or identity of indiscernible.

00:03:04: So, you know two things are the same if and only they have exactly.

00:03:10: But that's not really how mathematicians use this notion of being the same.

00:03:14: You know, mathematicians tend to be very metaphorical so too a category theorists.

00:03:20: if you have two objects that belong to the same category and they somehow Meaning, from the point of view all other objects in a category look same.

00:03:39: Even though they're not literally equal They might be isomorphic.

00:03:43: So there are examples.

00:03:44: In group theory you'll learn about different presentations Of groups that end up having exactly the structure.

00:03:50: And even if their presentation are different The groups are isomorphics and group theorists would consider them the same.

00:03:56: In linear algebra any finite dimensional any ten-dimensional vector spaces, consider it the same as any other ten dimensional vector space depending on choice of bases.

00:04:05: You know you might need explicit isomorphisms to identify them.

00:04:09: so that's sort one perspective what sameness means.

00:04:13: but uh... That often not even flexible enough

00:04:19: because it rings a bell.

00:04:21: or what did I just say?

00:04:25: The Leibniz principle suggests more intentional equality, so to say.

00:04:33: But as you know I'm coming from type theory and i am actually a big fan of this Leibniz principle.

00:04:42: because how do you describe the difference between two things which are called isomorphic?

00:04:53: You have to observe their internal structure.

00:04:57: In my word, you're not even permitted to do this.

00:05:00: So the principle of equality in discernibles is actually valid and intact here... ...in Hothide?

00:05:11: Yes!

00:05:13: You interrupted sort-of attempt to give a more classical account about homotopy theories.

00:05:18: I didn't mean.

00:05:21: Maybe we'll return to that, and then we can come back to new perspectives on Leibniz's indiscernible of identicals in homotopy type theory for instance.

00:05:30: But anyway all I was gonna say is there are mathematical objects that mathematicians working in the area would consider it be the same even though they're not isomorphic sort-of example.

00:05:43: everybody likes dimension as you know a typologist have certain bent.

00:05:50: you know, a coffee cup and a donut are the same.

00:05:53: I don't think that's a great example because those spaces are actually homeomorphic which is to say isomorphic in the category of spaces.

00:05:59: but an example i like better.

00:06:01: You know, these spaces are homotopy equivalent.

00:06:06: And if you're interested in sort of counting how many holes there are in the space or how many higher dimensional holes they're on this space?

00:06:13: The answers would be the same even though the thong is one-dimensional In some sense and pair of pants as two-dimensionals.

00:06:21: So what Homotopy theory's about it?

00:06:24: a language that allows to treat objects not isomorphic but equivalent or perhaps weekly equivalent has nevertheless been the same.

00:06:37: But anyway, what Torsten was referring to just now is you probably have a better sense of this history than I do frankly but maybe i'll describe it as some sort.

00:06:54: What I was imagining when we mentioned it earlier is, you know this the way equality is axiomatized.

00:07:01: in first order logic.

00:07:02: And so thinking of that notion of a quality as kind familiar and set theory where two sets are equal sort if only they have exactly same elements If the element has slightly different names but one-to-one correspondence That's not what equals means in set theory.

00:07:25: But as you well know, this is very far from how equal gets used on a mathematics paper.

00:07:31: if you read a mathematician's paper they'll often write equals when they really mean isomorphic or maybe even something weaker than that.

00:07:39: and there are other approaches to foundations using Martin-Liff identity types but without equality reflection, so intentionally rather than extensively that are compatible with indissernability of identicals and more flexible allow sort of a more metaphorical meaning of Equality.

00:08:03: Yeah yeah okay you obviously come from classical mathematical background exotic stuff like type theory later.

00:08:21: And I might qualify that even more strongly.

00:08:23: so the, you know... The mathematics curriculum in the United States which is where i'm from it's a bit different than elsewhere in world and part of that as an artifact of our liberal arts system.

00:08:36: So As undergraduate I was a mathematics concentrator meaning took more mathematics courses then any other topic.

00:08:44: but of the you know, thirty two-ish courses I took as an undergrad.

00:08:48: that meant twelve of them were math courses.

00:08:49: And i spent the rest of time taking music theory and queer theory in American intellectual history and modern British novel and various other things.

00:09:00: so... In this sort of condensed undergraduate mathematics curriculum there often isn't much study logic in foundations.

00:09:10: As an undergraduate, I did not study it as a graduate student when i earned my PhD and almost certainly could not have told you the axioms of set theories or millifrancalset theory... Not many

00:09:21: people can!

00:09:21: You

00:09:22: know?

00:09:22: As a postdoc ,I taught The Undergraduate Logic course which was offered in the department .I just didn't end up taking approaches to foundations and then sort of around the same time I was getting exposure to an interest in homotopy type theory.

00:09:41: And that's how i got into other perspectives,

00:09:43: you know?

00:09:44: So maybe...I know some part of the audience will hate me for that but for me it was quite quick already!

00:09:50: We mixed a lot of disciplines and am not a category theorist at all.

00:09:54: so come from.

00:09:55: said theory is okay if I ask would be fine.

00:10:01: a very rough idea of category theory for that part of the audience.

00:10:05: That's not there, and maybe if there is something like your own perspective in particular because you have a lovely introductory book Category Theory In Context which I guess many people take as good first step into this realm?

00:10:23: Great!

00:10:24: Yes i'd love to describe category theory.

00:10:26: so I think a big innovation that sort of separated twentieth century mathematics from nineteenth-century mathematics was the idea, if you're interested in a particular mathematical object like a group.

00:10:43: You might productively study it by considering also the homomorphisms between groups.

00:10:49: so this is an insight that i associate with Emmy Nerder among others.

00:10:53: and So even if you're just interested in studying properties of individual groups, somehow treating them as a collective and looking at the way relationships between one group another which are depicted using arrows with a domain being one group.

00:11:10: And a co-domain been an other group.

00:11:13: These sort structure preserving functions called homomorphisms.

00:11:16: that was sort of an important insight and led to new breakthroughs in group theory.

00:11:21: And simultaneously, a similar perspective was being applied.

00:11:25: another disciplines so you know topologists were interested in distinguishing one space for the other maybe by means of some sort of numerical invariant or polynomial invariant .And around the same time it was discovered that if your invariant somehow respected continuous functions between spaces then and had more powerful information.

00:11:49: So a way to describe what these discoveries are doing simultaneously is they're Moving from studying individual objects of a particular type, so groups or topological spaces to studying the category of groups are the category.

00:12:04: Of topological space is our category has both objects but also arrows sometimes called morphism Sometimes called homomorphisms between them that satisfy it few certain axioms and Unlocked the possibility of completely new style of definition.

00:12:21: So you can characterize constructions on the object in terms of their effect on the morphisms, for instance.

00:12:28: In fact you can identify everything you ever want to know about an object and a category launched category theory.

00:12:45: And then another thing that it can do is, It can help unify different mathematical disciplines.

00:12:50: so there are some facts That are true of groups and true of spaces and true vector spaces and two other things for exactly the same reason.

00:12:58: um...and its because you can abstract them to the level of a generic category and generic objects in, uh-in a generic relationship improve the theorem at that level of generality.

00:13:10: Uh so these are the proofs by abstract nonsense that we were alluding too earlier.

00:13:15: And its effect is it'll isolate aspects any particular mathematical discipline that sort of formal or true for very general reasons.

00:13:28: Or it can be understood via analogy to a completely other discipline from the aspects that are particular to that Discipline.

00:13:34: so

00:13:36: anyway, there's little note as you I guess.

00:13:39: You know this is category theory also became increasingly popular and in computer science Via functional programming where people usually use Haskell they see like Monarchs at front doors or whatever.

00:13:53: So that's different point of access, but it shows already as you said that's quite sort-of universal.

00:14:00: Yeah

00:14:02: That's right.

00:14:02: I mean You know category theory among other things is a language.

00:14:06: um...that allows you to very efficiently express some rather complicated constructions and It makes it easier to define And study new kinds of mathematical objects considered or weren't so easy to think about before.

00:14:21: So the sort of fundamental objects that one studies these days in algebraic geometry are defined using categorical language, same and modern homotopy theory you know?

00:14:34: In computer science there is some categories You don't sort of stumble across in nature, but you can build.

00:14:43: I'm thinking maybe specifically the Kleisle construction associated to a monad that handle computational effects In very elegant way.

00:14:53: So it's actually your way to structure programs and use computer of.

00:14:59: categorically is often just a way to modular.

00:15:06: And is it quite a bit, maybe different or similar type of mathematics you would say?

00:15:14: Is category theory useful to structure?

00:15:17: I think there isn't.

00:15:18: Or...

00:15:19: I guess i would say so and i mean i'm thinking growth index work in algebraic geometry.

00:15:25: In the mid-twentieth century he ended up creating A whole bunch of category theory in pursuit Of introducing new structures New techniques in Algebraic Geometry.

00:15:35: So absolutely

00:15:37: May flop with a very another knife question.

00:15:40: and every now you use sketched beautifully this idea of the bird's eye perspective And what makes?

00:15:48: Like.

00:15:49: is it possible to talk about all kind of structures or there even like in category theory at some point You need more complex Categories, and if I'm not mistaken.

00:15:58: This also part of this higher category theory or infinite categories Is their way to understand that.

00:16:05: as an outsider Is that only accessible after some category theory?

00:16:10: Yeah, so I mean there are certainly limitations to category theories.

00:16:14: So one of them is they deal with the general aspects of any particular mathematical sub-discipline not the particular ones.

00:16:23: There's an area called representation theory which is considering sort groups in terms.

00:16:29: Some, you know maybe about half of representation theory is very formal.

00:16:35: There's uh if you have a subgroup you can construct something called an induced representation and this is an instance of a very general category theoretic construction.

00:16:45: so the properties of induced representations can be proven formally sort of much more abstractly.

00:16:50: but then there are other aspects of representation irreducible representations of a particular family or groups, I can't always be understood using category theory.

00:17:04: So that's one sort of limitation.

00:17:08: Category theory is really collection of proof techniques and those techniques apply to some kinds of problems and not other kind of problems.

00:17:14: but another sort of limitations which leading us towards higher category theories are some kinds mathematical objects live in more complicated mathematical setting.

00:17:25: And so the first examples are either something like a topological space or at chain complex, um.

00:17:32: So for topological spaces kind of the default notion of homomorphism between them is uh Is a continuous function?

00:17:39: That's as a Function between the underlying sets of points that somehow respects the topology.

00:17:46: But That's kind of not the end-of-the story, so you might imagine two different topological spaces.

00:17:54: You know let's say one of them is the circle and the other one is the torus or this sort of surface a doughnut.

00:18:01: And we could have Two different continuous functions from the circle into the surface of the donut.

00:18:06: So I imagine like tracing out a loop on that the surface.

00:18:10: And depending on which specific loops you're imagining tracing on the surface of the torus, they may or may not be homotopic.

00:18:20: And a homotropic means that you could continuously deform one loop onto another without slicing through should be understood as it's also a kind of morphism, but its higher dimensional morphism that exists between the two continuous functions we were imagining.

00:18:42: And giving an extra dimension to this situation.

00:18:49: And then there's a notion of homotopy between homotope, which would be a higher dimensional morphism between these high-dimensional morphisms.

00:18:55: so we've gone from objects in dimension one to morph is our objects and dimensions zero two morphisms into mention One to homotopes in Dimension Two the hired homotopies in Dimention Three and four five and six.

00:19:05: that goes on ad infinitum.

00:19:07: uh...and if you ignore this higher structure or quotient out by this Higher Structure You're losing some information.

00:19:16: questions about spaces that really cannot be answered very well or at the level of ordinary category of space and continuous functions, but are better approached in a higher category.

00:19:29: The infinity category of spaces' continuous function on all the higher homotopies?

00:19:35: It's interesting.

00:19:36: I mean to naturally use an example from homotopy theory But you're not mentioning something like category-of-categories.

00:19:46: from a computer science point of view would be this, that's the way to look.

00:19:54: Yeah, so that's also another route into higher category theory.

00:19:58: So you know categories have a notion of morphism between them which is called functor.

00:20:03: but even in the nineteen forties The original paper on Category Theory it was not about categories nor was It About Functors?

00:20:10: It Was About the Higher-Dimensional Morphisms Between Functors Which Are Called Natural Transformations.

00:20:15: and yeah.

00:20:16: so Category theory Is itself A Higher Dimensional Subject.

00:20:21: Actually In soft-traditional category theory, people usually say that the category of categories is just a category.

00:20:30: And in The World I Live, this is sort of slightly wrong... What's your feeling about it?

00:20:40: I

00:20:42: guess i don't know what you're referring to.

00:20:47: So I think of the category of categories most naturally as a two-category.

00:20:51: Exactly,

00:20:51: that's what...

00:20:52: Yeah adding in higher morphisms yeah.

00:20:55: i guess you could say though one category is called Cartesian Closed.

00:21:00: so it has objects inside which are functor categories and inside those function categories have these higher dimensional morphisms accessed via just a lower categorical structure.

00:21:18: So an ordinary one-dimensional category that is Cartesian closed, it's enriched over itself and so in these internal ham objects you can access some sort of enhanced structure.

00:21:31: I Just meant because In the sense Equality of objects Is more complicated or in the hot language?

00:21:42: It's not a proposition.

00:21:43: And in this sense, the category of categories isn't just an ordinary category but as you say it's a two-category.

00:21:52: But that comes from these type theoretic perspectives and new view.

00:21:57: Yeah I mean another... You know so thing that i've practiced or engaged more over the past decade is computer formalization giving definitions about categories and constructions, about categories proving theorems.

00:22:17: About categories not just on pen-and-paper but interactively with a computer proof assistant.

00:22:25: so the computer proof assistants are often implement formal system called dependent type theory which is different approach to foundations.

00:22:37: I'm completely setting aside sort of categories in homotopy type theory, let's say dependent-type theory.

00:22:43: In the sense that it is implemented into computer proof assistant.

00:22:45: lean where identity types are propositions and you have proof for relevance of propositions.

00:22:54: but there is an interesting design decision explaining what a category objects of a category, and then there's the arrows in a category.

00:23:13: And so you could define a category to have a type-of-objects and a type of arrows... ...and then there are source & target functions between the objects and the arrows.... ...an identity function an composition function and some axioms and so on.

00:23:24: or You can define a Category To Have A Type Of Objects and Then Dependent Type of Arrows.

00:23:31: So given rather than having a type that consists of all of The Arrows In The Category Having for any pair of objects, a type of arrows from the first object to the second object.

00:23:43: And somehow that one decision has huge stakes for the way everything else is formalized thereafter in a way that I find quite interesting.

00:23:55: so... So i mean for instance like a lot of statements that one would write on paper particularly when we're considering sort between functors or you know, don't even type check if You take the second perspective where you're defining the morphisms to be a dependent type so to prove that one functor is equal to some other Functor and your proof firstly.

00:24:19: That for all objects in the domain category these functors act The same way on the objects And then on paper I would say and the same thing for the morphism.

00:24:27: So for all morphisms in the Domain category of the functioners act the same way.

00:24:33: But that statement now will involve an equality between a arrow and one HOM type, and you have to kind of transport along the proofs of Equality Between The Objects To Get Those Two Arrows To Belong To The Same Type.

00:24:50: Anyway I think this is sort of interesting feature when it comes to formalizing even one category theory.

00:24:55: in the Proof Assistant Lean which adopts

00:25:00: raise in question, we had on our very first episode of About Logic with Kevin Buzzard.

00:25:05: We did a discussion between Kevin and Thorsten whether you can or should use lean without opening up the foundation so to speak?

00:25:13: And I mean clearly for some mathematicians it works fine without opening anything then for others maybe not could say how is it input packages and start doing?

00:25:29: or do you always need to open the packages?

00:25:33: Right, so I have been formalizing some proofs in Lean but also another proof assistance.

00:25:41: And the reason I'm working on other proof assistants is because I am formalizing proof that just cannot work at Lean right now.

00:25:51: Particularly when it comes categories, you know.

00:25:58: You can give a definition of an infinity category in lean using something called the quasi-category model so that that definition exists.

00:26:08: but it's essentially like taking this notion of an infinite dimensional category and kind of compiling it out to the foundations of mathematics.

00:26:17: So traditionally we think of mathematical objects as built you know, with a bunch of sets and functions and structures and axioms and so on.

00:26:26: And the problem is that an infinite dimensional category isn't really built out of sets—you could sort of give it presentation or give it coordinates and pretend that its built-out of sets... You can build one set but not the most natural approach to definition —morally an infinite dimensional category should be built out of something called homotopy types or ANIMA, or infinity group voids.

00:26:55: Sort of these are topological spaces but really considered only up to homotope equivalents or a weak homotopia equivalent.

00:27:01: and in other approaches to foundations you know Homotopy type theory is described as sort of synthetic theory of homotopy types.

00:27:12: When you say, You have a type it automatically has this kind of higher dimensional structure and rather than build in laboriously It's just there.

00:27:20: And I can give them much more efficient definition Of what an infinity category is.

00:27:25: if Homotopy Type Theory Is the background language?

00:27:29: Starting from a simpler definition will also simplify formalizations.

00:27:33: So I'm part of two collaborative formalization projects attempting to formalize some infinity category theory in two different proof assistants, one of which is lean and the other of which has something called Resk or RZK.

00:27:45: And we've gotten a lot further in Resk even though The Proof Assistant as much more primitive just because the foundation system Is A Lot More Amenable To The Type Of Math We're Trying.

00:28:02: So I think this quasi-category approach is sort of what you would call analytic.

00:28:07: There's a concrete definition or what an infinity category it, but at the same time its almost unusable and i think that one of your talks was actually a bug in the definition which nobody noticed because no body did anything with.

00:28:29: Yeah, so the notion of quasi-category is definitely usable on paper.

00:28:33: And you know for students that it's kind of nice because its relatively concrete.

00:28:38: if your a student who uh... You know was very comfortable with ordinary one dimensional category theory and has maybe already met Simplicial sets by taking an algebraic topology course then you can explain what a Quasi Category Is.

00:28:52: but um.. It's kinda like giving.

00:28:58: I do use the term analytics, but it's like explaining infinity categories.

00:29:01: But we're choosing coordinates everywhere and the coordinates sort of don't matter.

00:29:04: And you want to make sure that your construction are independent of the choice of coordinates?

00:29:08: But nevertheless they're baked into the definition.

00:29:10: so You can from that notion You know state improve a bunch of theorems.

00:29:16: It often involves a lot of technical what would call combinatorics though its sort of a combinatoric of infinite sets.

00:29:22: So at combinatorialist might disagree But in a proof assistant, it turns out this is just very difficult.

00:29:30: So what Thorsen is alluding to the fact that closely related definition of a con complex which has an analytic perspective on infinity group words was wrong for maybe several years and because if anybody had tried to prove any theorems with them they would have caught.

00:29:48: But there were essentially no theorems that had been proven about quasi-categories or con complexes in Lean until very recently.

00:29:57: The main success is a master's thesis of Jack McOwen, who successfully proved to that if x and y are quasi categories... Or really why?

00:30:08: Is the only one that needs to be a quasi category than the sort of internal hom?

00:30:12: Y to the X as again a quasi-catagory?

00:30:14: this fundamental result.

00:30:18: You can't do anything in cross-category theory without that result, but there are a lot of details in that proof and it took I think a year and a half to formalize at still being PR'd into mathlib.

00:30:29: It really is just makes you feel despairing of formalizing anything more complicated than given.

00:30:35: how hard was this very fundamental thing?

00:30:39: so...

00:30:48: You get rid of the spoiler plate, or is it a different conceptual approach to do mathematics?

00:30:56: Right.

00:30:56: So one way to think about it as you're putting in convenient abstraction boundary around the notion of an infinity category which is well-known method and engineering I take In the literature, when researchers use infinity categories they often don't use quasi-categories.

00:31:20: They sort of prefer to... work model independently, so sort of implicitly in reference to some axioms that maybe haven't quite been written down anywhere.

00:31:31: Of things that ought to be true about infinity categories and have been proven in the quasi category model somewhere we hope uh... And were just gonna argue from those principles rather than explain exactly the effect these constructions on quasi-categories.

00:31:45: That's what is happening already literature.

00:31:49: But I should say that what's happening in the synthetic approach is kind of more radical than that, and the same way that homotopy type theory as a more radical perspective on Homotopy Theory.

00:32:03: then just saying we're going to introduce some axioms you know?

00:32:07: In Homotopy Type Theory the kind of meaning of the logical operations.

00:32:14: You know, when you say there exists some X and C so that for all Y and C x equals y in homotopy type three what means is something a bit different?

00:32:25: So firstly this exists.

00:32:27: interpreted constructively it provides you an explicit choice of point X and c. The for-all Y &C is interpreted in continuous fashion.

00:32:38: Um, and the equals x equals y is interpreted as that.

00:32:41: The choice of a path.

00:32:43: so we're saying I'm given an explicit point which i'll call the center of contraction.

00:32:47: So for all other points why?

00:32:50: I'm continuously choosing a path from X to Y And what that means Is this sort of sentence that in first order logic would it assert That the set C has a unique element.

00:33:01: In homotopy type theory interprets that the Type c is a contractable space, so sort of something more powerful.

00:33:08: And that's extremely convenient from the perspective of higher category theory when contractability is the only meaning of a uniqueness that ever makes any sense?

00:33:18: So similarly these kind of reinterpretations of logical operations mean in this synthetic approach to infinity categories explaining what it does on the objects is automatically a functor of infinity categories.

00:33:41: And that's something very difficult in pen and paper, like actually defining an explicit...functor between explicit-infinity categories as something you basically never do because there'd be infinite amount higher dimensional coherence checks which are completely infeasible.

00:33:56: you always use some trick appealing to some kind of universal property or some sort of magic reason why this functor exists.

00:34:02: But in ordinary one category, you often do just define functors.

00:34:06: You say for every object in the Category A here's the corresponding object and the Category B And For Every Morphism In The Category a Here Is The Corresponding Morphizm In The category b?

00:34:23: kind of reinterpreted the entire formal system, not just given axioms for infinity categories.

00:34:29: So you emphasized convenience again.

00:34:32: but what you described before is that like maybe it's a natural way mathematicians solve reason.

00:34:39: I mean as you say they're not really in detail analytics or analytical just use this reference.

00:34:47: But maybe they use some sort of synthetic, some half-baked synthetic reasoning and... Maybe the more developed synthetic mathematics is filling this gap.

00:35:03: Does it make sense?

00:35:04: Yeah I think that dream for the future in your account of development on this is very accurate.

00:35:12: new mathematics is sort of half-baked for a long time and you kind of backfill the rigor.

00:35:18: Yeah,

00:35:20: so I mean as i understand it like Cantor's work on infinity sort of predated a rigorous axiomatization of set theory for instance and you know a lot of the work on calculus kind of pre-dated a rigorous understanding of what calculus.

00:35:37: But I think the sort of modern hope is that as you kind of backfill these synthetic systems, they become formal to the point that you could teach the rules to a computer and then build a computer proof assistant.

00:35:53: That would then allow you to rapidly confirm or try to prove false and check the consistency of these axioms maybe in an empirical way rather than met a theoretical way, you know.

00:36:11: and also just get used to the new synthetic framework.

00:36:13: So in my personal experience of learning homotopy type theory I first heard a lunch of lectures and then read pieces of The Hot Book.

00:36:22: Then I taught a course in homotopy type theory, and as a challenge to myself wrote all the problem sets for this course using Agda.

00:36:41: And so I spent like... A lot of time every week sort writing and solving these Agda problemsets that was developing.

00:36:48: Did you use

00:36:55: cubicle or was it just vanilla?

00:36:58: No, vanilla agda.

00:37:01: But with the feedback of the proof assistant ever since then I feel very confident now doing pen and paper homotopy type theory because i have this experience where a bunch of slightly wrong ideas were corrected by.

00:37:16: So I find also, for me it's a good way to teach certain things because the students can as you say intuitively learn what is correct way of reasoning without having to see any so formal rules.

00:37:34: The tension here that gives an informal explanation but there often we are informal and unsound.

00:37:44: Or you can say, okay we have a performance system but who understands the performance system?

00:37:48: But then this computer's proofsystem is sort of nice middle ground.

00:37:52: You acquire intuition words with correct proof by using it and maybe don't actually need that anymore because you've acquired this intuition now

00:38:02: Right, and of course like it's also nice to get immediate feedback.

00:38:05: I mean that you know a big problem in mathematics pedagogy as students do homework And then by the time they get back a week later nobody is thinking about the problem anymore.

00:38:14: It's much nicer to be corrected immediately.

00:38:18: That's embarrassing because its just computer not tutorial.

00:38:24: Actually related to this are using AI.

00:38:27: have your tried to do proofs?

00:38:32: AI implementations like?

00:38:36: Yes, so currently there are auto-formalization agents that are targeting Lean.

00:38:42: There's not anything specific targeting other proof assistants I'm aware of but i have been experimenting a little bit with AIs targeting lean in couple different capacities.

00:38:53: So you know...I've been testing their capabilities with ordinary one category theory.

00:39:00: just you know, initially I was kind of very skeptical that these systems would be able to do much of anything just because one category theory it's more about constructing definitions than proving theorems and Lean treats those two activities somewhat differently.

00:39:17: And indeed that does seem to be a limitation for some of the auto-formalization agents.

00:39:23: More recently i've been testing whether pen and paper arguments involving simplicial sets in quasi categories, whether some of the sort of invisible mathematics could be automated away with AI.

00:39:41: I've not had a lot of success there yet, I would have to say just because I think they are kind of a lot technical details but... But I should say that much prefer interact an auto formalization agent than a large language model in discussing mathematics, because the large language models will feed you a lot of bullshit.

00:40:06: And in particular just... In the last few weeks I've been currently in the process of revising my category theory book and trying to develop a few new counter examples.

00:40:21: so if drop hypothesis X from theorem Y um, conclusion Z is false.

00:40:28: That sort of thing and you know when I uh You know.

00:40:31: so first thing i should do is to literature search.

00:40:33: Do these counter examples exist in the literature?

00:40:36: And Um Uh you know.

00:40:39: if If something isn't a literature our large language model Is pretty good at surfacing this but it's not in The literature.

00:40:46: It'll sort of blame the literature for the fact that its Not able To come up with A counter example.

00:40:52: Right, so that's it would say you know.

00:40:53: but this is a well-known mistake in exercise six point two point v of reals category theory and context.

00:40:59: So then I go to the bookshelf.

00:41:00: And indeed there's no exercise six points two point.

00:41:02: being inside i did not make a mistake But anyway at some point I sort of gave that up and came up with my own counter example harmonics, which is one of these AI startups agent Aristotle to verify it for me and lean as a kind of extra check that my counter example was correct.

00:41:24: I did not ask a large language model for this because if they tell me it's correct i feel like gives no assurance really.

00:41:32: but indeed you know this something in one category theory and Aristotle was able to confirm.

00:41:39: I

00:41:42: mean, this is a nice combination of AI and formal proofs because if you do test the AI as long as they can produce formal proof then it's trustworthy.

00:41:57: Well so there

00:41:59: are some caveats that experienced users are well aware but state for the record.

00:42:05: So you know caveat number one, so what the AI is producing as a source text or that user input texts to our computer proof assistant and your relying on uh, stated proof in fact proves the stated statement.

00:42:28: Um it does not verify that the stated statements is one that was intended and particularly if you know part of what your auto formalization agent doing as providing new definitions its quite possible.

00:42:40: um that this statement is wrong an-and this could be a relatively innocuous way.

00:42:44: so for example my teaching I was preparing a demo for my students of formal proof in Lean that the square root of two is irrational.

00:42:52: And so, I open up my lean file and write theorem squared to two is irrationally.

00:42:56: then i'm in middle writing the proof.

00:42:58: all sudden notice some things are suspicious.

00:43:02: it turns out Various different versions of the square root function.

00:43:10: One is in the namespace, you know It's sort of rational dot square root.

00:43:13: and what it is?

00:43:14: Is its kind of like some sort of Rational approximation to that function.

00:43:19: And that's the one that I had used in this statement.

00:43:21: So so The theorem as I had stated at squared if two is irrational was false because for this version Of the service a rational function.

00:43:28: It wasn't fact true You know, so that was a mistake that I made.

00:43:32: not an AI but But when Complex definitions are involved.

00:43:36: You really, really have to check that they mean exactly what you think they do.

00:43:43: The other thing is we've seen a few We meaning the lean community has seen a Few examples where an AI kind of tries to cheat somehow.

00:43:53: so you know A thing that it could Do for instances add an extra axiom, you Know axium zero equals one to the top of the file presented in a kind of obscure way and then And then it can prove whatever you want, and it'll pass the type checker.

00:44:07: because certainly assuming zero equals one.

00:44:09: Whatever you're trying to prove is true or other behaviors like

00:44:16: that.".

00:44:16: It could exploit a reasonably discovered inconsistency in the proof system world I mean?

00:44:21: Right exactly!

00:44:22: There's always the possibility of bugs on the kernel.

00:44:24: so anyway what would certainly go into the record saying is that an auto-formalized proof.

00:44:30: I guess, maybe depending on the subject area.

00:44:38: There's some areas where you know that mathematics library just is nowhere near this statement and so there's no chance of a statement as correct in which case auto formalization is sort fantasy from start but within domain covered by human engineered mathematics library an auto formalized proof more reliable than natural language.

00:45:01: But you know, but there's still a role for human referees.

00:45:05: Actually I wonder because we talked about lots of convenience that since setting mathematics more convenient... ...but if you have just so enough AI on it then maybe this problem sort disappears?

00:45:17: Because the AI is just happy to prove everything with quasi categories which humans would not be able to manage, right?

00:45:26: Yeah.

00:45:27: I strongly disagree with that.

00:45:29: There's definitely a role for AI in formalization which is to make it easier.

00:45:34: you know... Right now sometimes people talk about the de Bruun index which technically like the amount of lines lines of natural language proof, I think a more relevant factor is how much time it takes to write a formal proof versus an actual language proof and everybody working in the space would prefer it take less time.

00:45:54: And if AI can help with that?

00:45:56: That'd be great.

00:45:57: but proof quality still matters.

00:46:00: you know there's no permanent place for ugly mathematics.

00:46:08: The process of formalizing is not just about checking that a theorem is true, but building a library that's usable as the basis for further formalization efforts and code quality there matters enormously.

00:46:21: And so I don't want sloppy unreadable incredibly long proofs.

00:46:27: some fact in quasi-categories—I think it's worth understandable to humans and can be used as the basis for getting into the frontiers of mathematics, research frontiers in mathematics.

00:46:43: I wholeheartedly agree with this but there was a discussion on computer science right?

00:46:48: So we have so if you try two uh i mean such high-level programming languages which support abstraction and so on which is similar to what you already described.

00:46:57: in mathematics We like to write programs nice But actually now with AI, you can generate these programs.

00:47:06: And then the question is do we need this high level languages because they are able to produce a similar code?

00:47:14: Which maybe not as readable but in the end what matters?

00:47:17: I mean that's different

00:47:26: than mathematics.

00:47:31: won't accept a future where the only formal language system is lean.

00:47:35: Sure, I agree but there's this tension and possibilities that all these high level stuff actually doesn't really matter so much anymore because AI approaches the gap.

00:47:49: It's not a future I would like But it's possibility.

00:47:55: Just the tiny remark.

00:47:57: we had similar discussions when computer usage In general, anti-mathematics for color theorem was celebrated but also hated because some mathematicians said we just have this huge case distinction.

00:48:10: But then the lovely beautiful problem is that now and high class mathematician won't touch it.

00:48:16: maybe they would've found out new techniques or deeper understanding of whatever.

00:48:23: Then later even though try to re-proof it, shorten the amount of cases needed and things like that.

00:48:34: No I had a bit more personal question which is a question for you as a woman.

00:48:42: obviously in mathematics there's still gender imbalance.

00:48:49: maybe can you comment on this?

00:48:51: Do you think something should overcome or if so how?

00:48:58: Yeah, I guess i will say.

00:49:01: I still think it is harder in some ways for a woman who has Intered mathematics to kind of find interested in mathematics To find her way into the community than It Is For Some other folks.

00:49:14: you know?

00:49:14: I Know A lot Of Young Women Who You Know Feel That Extra Pressure Whenever They want to ask A question In Class instance that you know the sort of quality is a question or The fact that the question reveals but they haven't already understood something will then reflect Negatively on, you know their entire gender.

00:49:39: I think that's still a very very real experience and you could imagine Sort of two parallel students one Of which it feels like we can ask questions with abandoned And one of which can never asked questions at all?

00:49:50: And you know who's gonna be in a better position a few years down-the-road Not so much within the math research community, but at lower levels.

00:49:59: I also hear a lot of stories of students who are sort of explicitly discouraged from going into mathematics by a teacher in high school or somebody trying to push them to take easier courses.

00:50:12: Or say this isn't really for you... It's shocking that still happens and it does happen.

00:50:18: At more advanced level what means is make it are kind of tougher in some sense, have maybe spent more time thinking about like do I really want to be a mathematician?

00:50:33: Is this is the career that i'm looking for?

00:50:35: and then you know tend to have the persistence.

00:50:38: And um To kind of carry through because they've already sort of had You know thought critically about whether there's may be some other use of their time.

00:50:46: So yeah think we should still be mindful, you know not just along the gender axis but among other axes about how kind of different experiences might affect our students and who's encouraged to continue.

00:50:59: I certainly have a lot more fun at conferences where there are more women...just sort of socially.

00:51:07: i think it makes a difference..I feel less pressure when i'm asking that question in a conference if there is a lot of other woman on the.

00:51:16: But we're trending in the right direction.

00:51:18: And I think as long people are still kind of mindful that not everybody gets to the classroom and with the same experiences, things will continue to improve.

00:51:29: Lovely educational comment or comments on education?

00:51:32: Or whatever you would phrase it... May i ask is there anything else you'd love to speak about where we missed when we were too narrowed

00:51:40: into

00:51:41: a math?

00:51:43: Maybe I have question for you.

00:51:48: I mean, there's something that i'm curious about which seems to be kind of a...I don't know how to describe this but sort of like historical or sort of practical or circumstantial split between the type theory community and set-theory logic.

00:52:10: community.

00:52:11: I don't know if this is part of your experience, If you have any explanation for it?

00:52:15: Um i'm very curious about how This came About um or if i'm Accurate and describing It that way And i guess i mean maybe within Mathematics as opposed to Within uh computer science.

00:52:28: um i think i mean That's a great question.

00:52:30: i Have my own account but i'm not sure whether it's historically accurate.

00:52:35: So

00:52:36: shall i start torsten?

00:52:38: yeah Yeah, so I guess i came from the satirist side of things.

00:52:43: And I mean um...I would say two things.

00:52:47: whenever some mindset or tradition is kind-of dominant they might not look at the others for their next tradition with full respect that they should.

00:53:00: It's generally true it isn't really only on satirists but okay there are these weird category stuff.

00:53:07: But I don't really care.

00:53:08: I can do everything in principle, and rightly so.

00:53:11: i guess In some sense you always reinterpret and emulate things.

00:53:17: Of course on your high level You see where this emulation misses a tiny spot or isn't fully accurate.

00:53:23: but then there was not as much communication which would have been good And we had contingent factors like one mailing list whichever with the set theory dominant and category comments get discouraged, then people start their own forums or communities.

00:53:46: Then we have a lot of more division than necessary so to speak.

00:53:53: The other thing is maybe that this category theory had more interest in desire physics things.

00:54:05: We just needed the foundation to prove a point, but we never really used the foundation right?

00:54:10: Didn't touched it.

00:54:11: But that's only my historically inaccurate account.

00:54:14: So Thorsten what do you think?

00:54:18: Can I add more...I see you asked about community..but i would like to add personal perspective.

00:54:24: Actually give talk.

00:54:28: few years ago at Lambda days in Krakow and started with programming languages, CV and I tracked down what programming languages i have been using.

00:54:38: And then started with language code basic and some money doing assembly programing... ...and then was not satisfied with these languages and looked for better ones and ended up with functional languages like list programming and type functional languages etc.. And this is, I guess that's my interest.

00:55:02: So always...I'm sort of looking for the perfect way to express yourself here and in this experience it seems to me that people are quite stuck with a foundational system which has been developed almost hundred years ago now.

00:55:28: And don't question whether this is really good way to express yourself.

00:55:34: For me, it's quite important to choose a good language... ...to express your self and I mean for me the analogy as when i was doing assembly program in Alan C., that's how you should tell people they shouldn't use C or not assembly programming but we can do everything!

00:55:54: which you need to do.

00:55:55: We can do an assembly, why would we learn a high level language like C?

00:55:58: Which was more high levels than the assembly?

00:56:00: and this in a way reminds me on the same just or not the same but analogous justification.

00:56:07: yeah...we can do everything.

00:56:09: first of all logic and sets theory.

00:56:11: so I wouldn't be learning anything else.

00:56:13: And i think that language and leverage of languages is quite essential for making progress.

00:56:21: Yeah, I guess my personal perspective is you know with AI there's gonna be an increasing emphasis within mathematics on computer formalization.

00:56:29: and with Computer formalization.

00:56:31: There's going to be an increase in importance and emphasis in mathematics on Foundations and expertise in foundations but explicitly including type theory because that seems to sort of predominate amongst the formal systems used by computer proof assistance.

00:56:46: So I would love to see more expertise on foundations within mathematics departments in general, and sort of type theory.

00:56:57: In particular you know not because I see a future where we have one foundation for all of mathematics maybe with type-theory replacing set theory but instead kind mathematicians can experiment with, maybe the aid of a computer proof assistant.

00:57:17: Maybe by developing domain-specific languages to shorten and simplify formal proofs in their particular domain... If you're implicitly using a foundation system to prove a theorem on paper then it's okay that you don't understand at certain level depth but I think we need more real expertise.

00:57:38: so I'd love ideas for how to kind of bring type theory back into the fold and also reinforce sort of other approaches to foundations at the same time.

00:57:52: But yeah...

00:57:54: Yeah, I think pluralism is a theme that comes up often in our podcast which might be tiny empirical evidence.

00:58:03: you are right on their direction Great.

00:58:08: So I'm really happy about this talk, i learned a lot.

00:58:11: sorry if i slowed down the discussion

00:58:13: it was that was a useful intervention so thanks for that.

00:58:16: okay

00:58:17: yeah.

00:58:18: so um there is no urgent thing to say.

00:58:22: thank you

00:58:23: very much yeah

00:58:24: and thank you for being here and have a great week!

00:58:27: Okay Thank You!