Patrick Shafto

In five years, if that project is successful, how will math have changed?

I've already alluded to what I think is the biggest change, but that's outside of math. Inside of math, I think there are a variety of consequences that are interesting. So one of them, that's a favorite of mine of late, is making the point that the actual relationship among mathematical papers is almost entirely implicit in the literature.

So I might say I borrow

Hmm.

lemma such and such from such and such paper. What that actually means can be quite ambiguous, right? Like you might borrow the sort of essence of the argument rather than the exact argument they used, these kinds of things.

Mm.

And so while you might call out to other results across the field that yours depend on in interesting ways, that structure of dependence has been implicit.

as we translate to formalized languages, all of a sudden that's explicit. So we have like a graph of mathematics and the dependent structure among arguments in mathematics.

Welcome to Tastebench. I'm Philip Zahn, my co host is Bruno Marnette and this is a podcast about Taste and the creative side of AI. Today's guest is Patrick Shafto Professor of Mathematics and Computer Science at Rutgers University. He is also a program manager at DARPA, where he leads the Exponentiating Mathematics Program. Its goal is to radically accelerate progress in pure mathematics, the topic of our conversation.

It's a pleasure, Patrick, to have you on the show. As a first question, can you describe what you're currently working on and what your position currently is?

Sharia, thank you for having me. This is very exciting, looking forward to the conversation. at the moment, I am a professor of mathematics and computer science at Rutgers, that's a state university of New Jersey. and I am on loan to DARPA, which is the Defense Advanced Research Projects Agency in the United States, as a program manager.

and so in both places I'm I'm interested in things at the intersection of AI and mathematics. so in in my research, you know, it's mathematical foundations for AI.

in at DARPA there are two programs that are related. One is exponentiating mathematics, which is about AI for pure mathematics, AI informalization for pure mathematics, and then the other is called AIQ, Artificial Intelligence Quantified, which is about mathematical foundations for AI.

When I saw this correctly in your CV, you moved a bit across fields over time. Am I interpreting this correctly in the sense that you also had publications in different parts that are not typically associated with computer science? How did this transition happen?

Yeah, I mean I I'm I'm interested in the question of of learning. and and that doesn't have a unique home in the disciplines that we see as traditional. and so the question I've been interested in has been the same. The best place is to be thinking about it and pursuing it from the perspective of like where y where can one make progress?

have shifted over time and at least from from the things that I see and am well positioned for. So that's

Very well.

led me to a an interesting career path where I've had tenure in in multiple departments.

Yes, which I mean, I was just stuck by it because in these days that's not the normal thing to see. Right. That's why I was asking.

Yeah, it is

quite quite atypical. I live now in

mathematics and computer science, but functionally it's a pure mathematics department.

And love if you could also say a few words about DARPA because it's a very iconic research institution. But I don't know if people really know the modern days DARPA.

Yeah, yeah. Yeah, DARPA, again, it's the Defense Advanced Research Projects Agency. So it's a a funder of research in general in the United States. it it has the name Defense in it, but really the mandate is much, much broader. so the there's a historical event that I think is is informative to like what DARPA is and what its goals are, which is the the thing that actually launched DARPA in the first place, which was Sputnik.

So the Soviets launched obviously rockets into space. and and this was a great source of surprise for the United States. there's a lot of details one can go into there about what precisely the surprise was and to whom, and so forth, but suffice it to say it captured the public's attention in a highly negative sort of way. and so

It's not a military event, of course, but it's a technical event that has many consequences, from military to economic to you know, just general questions about security and where you know where we were vis-a-vis the Soviet Union at the time in terms of advancement. and so DARPA was started

to you know they sometimes class it as take surprise off the table. If there's something that seems like

Hmm.

it's potentially possible, we want to be the first to try it. and and show that you know it can or can't be done. And so

I see

already the parallel with the kind of AI revolution and the kind of panic people could go into.

Yes.

So yeah, DARPA has done a number of iconic things over time. One is, you know, invented the internet, they as they say, but is a real supporter of the first version of the internet. GPS is another good example, came out of a DARPA program. Siri, that was another spin out of a DARPA program. autonomous vehicles were to a large degree motivated by a couple challenges that DARPA ran in the early

2000s, 2010s. So yeah, it's done a variety of things. It's been a funder of AI for, you know, as long as AI has been around almost.

Hmm.

And of course, what that means over time has changed. But you know, especially in this moment where AI has things moving quite fast, you know, DARPA has a big role in trying to understand.

what is the frontier, what is around the corner potentially and trying to, you know, make sure we we are the ones trying to take those big risks to establish what is and isn't possible.

You wrote an essay last year called The Infinity Project about the future of math. Can you describe the overall vision behind it?

Yeah, so the Infinity project is is really thinking about what happens when we move mathematics from from living in journals and textbooks and human heads and as we project it into code. And that that bridge there

Mm.

is referred to as auto-formalization, right? So the automatic translation of say natural language math into a formal verification language such as lean.

and so you know what I was observing at that time was that auto formalization technology was getting better. You know, it was still quite limited at that moment. roll forward just a few months, you know, I think we're seven, eight months down the road, but like you know, that's auto formalization technology is is quite real. and so it's it's one can see that you know that's going to change mathematics.

Can you briefly describe it? So that our listeners understand what it actually means.

Yes, yes. Auto formalization is translation of natural language math into formal verification languages such as lean. so of course, math has traditionally lived in papers, much like other fields, except that you know other fields also have some kind of at least scientific fields have some kind of software-related artifact, usually or often.

Math is not that way. It's you know, mathematicians, that's that's your tool. and and that's that's problematic because if you look at a math paper, it's full of mathematical symbols and so forth and arguments that are really it's very hard to understand anything, even for trained experts.

Hmm.

and so the ex the

The accessibility of mathematics is extremely, extremely limited, especially as you get close to the frontier. And what auto formalization will do is automatically translate from natural language mathematical text, as we've been practicing for decades, centuries, into languages, programming languages, such as lean. There are a number of them, Isabel, Rock.

Agda, there are a variety that have this general capability, but lean is sort of the standard of the moment. And when you translate it from that natural language into the programming language, that changes the accessibility. What it means to have a proof in a language such as lean is for it to compile. And so you have feedback about whether your proof is a proof or not.

.

Which in natural language math, there's no signal there, right? Like you need to know, right? And that's what mathematics education at the graduate level and above is, is really indoctrinating people into the culture of being able to prove things in a way that we believe that they are in fact true.

In five years, if that project is successful, how will math have changed?

So I've already alluded to what I think is the biggest change, but that's outside of math. Inside of math, I think there are a variety of consequences that are interesting. So one of them, that's a favorite of mine of late, is making the point that the actual relationship among mathematical papers is almost entirely implicit in the literature.

So I might say I borrow

Hmm.

lemma such and such from such and such paper. What that actually means can be quite ambiguous, right? Like you might borrow the sort of essence of the argument rather than the exact argument they used, these kinds of things.

Mm.

And so while you might call out to other results across the field that yours depend on in interesting ways, that structure of dependence has been implicit.

as we translate to formalized languages, all of a sudden that's explicit. So we have like a graph of mathematics potentially. and the dependent structure among arguments in mathematics. And I think that's really cool. That's an entirely new field that we could study.

It seems, sorry, just a quick comment on this. It seems also from a learning perspective, a very different way of kind of tracking the results in that form, instead of relying on this kind of ephemeral thing out there that you learn through hard years of being exposed to it indirectly.

Yeah, absolutely. The artifact itself, right? Where in contrast with math now, which is a very like the artifacts we produce are very localized to the thing that you're proving. and only later get integrated in some kind of gr global structure, if at all, right, as it gets distilled into textbook-related, you know, subject matter.

as we move toward formalization of of the whole of mathematics or a large, very large portion of it, you'll have that dependence structured locally and globally immediately. And that's quite cool.

Can I ask about the scope of the auto formalization? Because what I remember from my academic days when I was working on verification was that at the time, the real focus of formal math was theorem proving almost exclusively, right? It was all about proving tautologies. But obviously there's more than just proofs in a math paper, right? There is interest, there is opinions, there's conjectures. Is the...

Are you specifically working on the proving part or are trying to capture the entire paper?

We we actually don't talk that much about the proving part, not because it's not important, but because it has been pursued for decades. right, this is a a r relatively old literature, back to the 60s

Exactly,

at least. and so what we're really interested in is sort of two things. One is the auto-formalization that I've talked about. Suppose you have a precise mathematical statement, can you translate it? And then presumably the question is, can you then produce the proof that it asked for?

but the other one is where do those abstractions come from? Where do your lemmas, propositions, and theorems come from? How do you decompose a theorem you want to prove into a candidate substructure?

you

so in math, we think about this as a proof sketch, perhaps. in formalized languages you have lean blueprints. that sort of are you know the artifact that describes that in the formal setting.

but it it speaks to a thing that I think is actually like very human, right? mathematicians

Mmm.

often wax poetic about the beauty of certain lemmas and certain kinds of arguments. and that's always been like you know poetry, more or less, right? Like it's a matter of taste somehow. although there, you know what makes something beautiful does have it's not like, you know.

without any grounding, right? You want if you want a good lemma, it should be not strictly speaking bound to the situation that it's being proposed

Mm-hmm.

in, because then it can't be generalized very easily, can't be borrowed and used for other sorts of arguments. So you need to be abstracted a little bit from the context so that it can be reusable. And those are two clear criteria that are valued. But

you know, it's entirely open as to whether those exhaust what we think of as beautiful or or useful lemmas, or you know, theorems or propositions. Whatever.

guess

coming from a computer science background, I have a bit of a bias because I always think of an isomorphism between proofs and programs. And I always wonder how much modularity in computer science is thought as relatively solved, with the idea of importing code to use it in another place, or having type system that makes sure everything fits together. If it's possible, maybe it's going too technical, but is there a way to...

explain why it's not so easy with math, why it makes math kind of harder than combining programs in computer science.

There's there's a couple ways to sort of answer this question.

So what makes math different from just computer programming is is one way to sort of think about it.

Yeah.

So one is the foundations of mathematics are not settled yet.

Interesting,

and so if you want to implement it in computer code, right, like you might have to change that over time. and so

Interesting, interesting,

right, there there's a lot of active work in homotopy type theory, for example, which is meant

maybe the leading effort to try to integrate math, pure mathematics and and computer science. but it's still a research area. So there there's that piece of it. I think the other thing is that, you know, mathematics has a tradition that I think is quite beautiful that computer science didn't inherit, but I kind of wish it would. And and it's that mathematics over the years compresses ideas down to a standard set.

A relatively standard set of subject areas and tools that every argument in principle can be built out of. Right? And so this is partly out of necessity, right? Because math has to live in human heads to some significant degree. And we've gotten to a point right now where no mathematician can operate at the frontier of all of mathematics. But

You know, to deal with that over, you know, the past hundred years, we've established sort of standardized ways and and tools in which we can talk about the breadth of mathematics. So I think like set theory and category theory are sort of like standard foundations, but also like we also care about certain areas of mathematics as being summarized and standard, right? So everyone learns some analysis, some topology, some geometry, some algebra, right?

And that's a standard curriculum at the graduate level

Mm.

in across many US universities at least. And this is in part so that you know everyone graduates with a PhD, being able to speak about certain kinds of results that are old and venerable in a way that's

Mm-hmm.

mutually understandable.

Mm.

Right, when you get to the frontier, it's always going to be a little bit more messy and chaotic. But you know, at least we can have a common trunk of mathematics as we climb up to the branches. and that's kind of the idea. computer science doesn't really have this in in the same sort of way, right? Like computer science is a very functional exercise where like you want code to do something, and so you just write it. And

It's not without any standardization, of course, but it hasn't really been necessary to standardize in quite the way it mathematics has.

And maybe just as a transition towards more AI specific topic, when you talk about standardization, this is all about human understanding, right? When you start transferring a paper to a machine readable format, do you still care about preserving what makes things understandable to a human or do you allow yourself to simplify to just whatever the machine needs to understand?

I think this is a great question. and it it's open at the moment. and you know there's no way to sort of close it fully. So like I think this will be an ongoing debate for many years. there will be certain places where we just get proofs because we want a proof, right? formal verification of software is a good example where like one can imagine I just need a proof of some small thing, and like the

The elegance or beauty or reusability of that is somewhat beside the point, potentially. so that's a sort of place where where I think we may not care so so much. at least possibly. But I do think we will want computer science to move in the direction of standardization along the lines mathematics has been, at least to the extent we want formally verified software.

Because we're going to have to recompose arguments, because at the end of the day, we're writing software in order to do stuff for us.

Yeah.

And systematicity has roles both in human readability and in just good software practice and good math practice also.

Speaking of writing code, as of now, can you walk us through how a typical interaction, what a typical problem that gets tackled with the existing tools looks like and how an interaction like with these tools look like?

So at the moment in math, there's no standard interaction. There's a variety of ways one can enter to try to use AI tools and formalization tools depending on what your needs are. And so I guess the most standard one is people just interact with language models and ask them questions.

This is very simple way of going about things, but it's quite powerful, right? Because no human has read the entirety of the math literature. And we know for a fact that arguments are sometimes reproved, right?

Hmm.

and you may not know it, usually you don't, because if you did, you wouldn't go through the effort or you'd redo it in the way that was done before to check it, right?

Mm.

and so

that alone is a huge contribution, and many people have talked about this as being you know incredibly valuable. it's also notoriously difficult, like if if the proof exists in an adjacent field, right, the the leap is like both recognizing that there's a proof and

Hmm.

rocking all of the you know details of that field in order to really see that is the case. and so that that's I think the biggest one right now.

is you know people just you know asking models and you know GPT5.6 is is very very good in in interesting ways it's worth playing with others are good too but you know that one just came out a few days ago and so it's on my mind. and so you know I think that's the biggest way. There are other ways that one might go about this, right? So like suppose

You have an argument that you don't that's very complicated and technical, and you want to be sure that it's correct. That's another motivation to engage with the formalization tools. So there have been examples of this also.

One that was well reported on was Peter Scholze's work in condensed mathematics. there's a hard technical piece that was sort of not the entirety of his proof, but you know, or the mathematics that he was developing, but like there was one piece that they wanted to make sure was correct. And so they undertook a manual formal formalization effort, this was several years ago now, in order to check all those details.

So that's a different angle, right? Like it's entirely manual, entirely informalization. And then of course there's sort of the passing back and forth between those settings where you might want to, for example, take a known paper that's just been written and translate it into a formal setting. And AI can help with that. Although there are things that one needs to be careful about.

there's also mathematics that lives in code that you might want to translate back out. So like Mathlib is a library

Hmm.

of mathematics, formalized mathematics, and you might want to port ideas back out into into natural language. And so that's informalization.

And those are those are a few of the ways that one might interact. And of course, you might do any of those interactively or repetitively.

Yes.

In your opinion,

there, is there, is there also a good results already to have in the more, in the earlier stage of a, a, a,

Yeah. People people interact with language models around this kind of activity. I think it's accurate to say still the experience is relatively mixed. it's mixed for a few reasons, one being, you know, just certain areas of mathematics it's better for that and others less so. I'm not totally sure why that is, but you know probably.

To the training data, other sorts of things that we don't have access to. but the other thing is that you know mathematics arguments are are hard and subtle, and so you know it can be useful to bat those things back and forth. but you know, models make mistakes in ways that are not entirely like what humans do. So

that can be a little bit tricky to manage.

In the making of mathematics that has been dominated by humans so far, there are all these questions like what is actually problem worth solving, what are useful abstractions, etc. It's clear that if the technology in AI evolves, so must, in some sense, also this of merit system evolve. What are your thoughts on this?

think this is a really great question. So I guess, you know, one point in in this space is there's a wonderful paper that was written by Akshay Venkatesh a couple years ago on the f I won't remember the title exactly, but it's on automation and mathematics. and he introduces this idea of LF

Go, I believe, or LF1, which is sort of like an idea of having an AI model that's as good or better than a human. And then the question really is like, well, what's important? Does that change in terms of like mathematics, but also in terms of like what we do as mathematicians? And he has this interesting economics argument for like what matters in math is basically like, is it hard? Right? Lots of people have tried it but can't quite get there.

Mm-hmm.

and then does it have consequences?

Mm-hmm.

and and like right in some some sense it's a sort of supply and demand kind of thing, right? Like it's

Absolutely.

wanted by many, but and it would

It's hard.

you know produce new mathematics that would be of interest, yeah.

extremely hard to produce.

and so that's that's I think one way to sort of think about it.

I think there'll be other pressures as well, potentially. right. So that's I think a very high-level sort of argument that I I agree more or less with. but I think you know we as mathematicians will all want to be able to access our own corner of the mathematical world in a way that allows us to

think and do interesting mathematics, whether that's on our own or with AI. and so I think there'll be a lot of interesting action in domains that'll that will amount to thinking through, you know, what do we bet as on as being generative or important, where the consequences are much less known than a

you know, well well known, famous conjecture where the details are often already worked out. somehow.

Can you maybe zoom in on the word hard? Because there's something about mathematics which is, I don't know, always felt to me, again, very related to humans in the sense that, you know, if an alien species came to us and looked at math papers, and if they were much smarter than us, they would discard many papers as, this is just a tautology, right? It just obviously comes from the assumption, And so think what makes us appreciate math is it's like this hardness that you mentioned. But I wonder how much this...

potentially, are you thinking of it as kind of a moving target? Like as AI gives us more IQ points, we just move the target of what hard means. Or is there a more stable definition of hard?

Yeah, I mean I think I mean I think hard is always a relative term, right? So that's you know, that I think is reasonable. You know, the fact that mathematics is hard, I I think is not intrinsic to

I don't think of as intrinsic to mathematics itself. Right. So if if we made it somehow easier, we'd math would still be math. in the sense that, you know, the the way I view mathematics is it's a tool for understanding the world around us. and that world can be other math. it can be the rest of you know the outside world, right? Counting in space and and all of those kinds of things.

So I think the essence of mathematics will will remain. I think it it's possible that what is hard about mathematics is going to change a little bit, right? Like math is viewed as hard in part because arguments have to be true, right? Provably true. And proofs have to convey that n they don't just have to be right, but they have to be understandable to other people. Otherwise they're not a proof in in the mathematics that we live in today.

and I think that bar is going to go down a little bit, right? Because formalization languages give you a clear signal as to whether a proof is correct or not.

And and and what that means is that you know some piece of that difficulty gets taken away or reduced at least. There's still lots of other things that are difficult here and interesting. but but that one, which has been so dominant in in math and math culture and education and so forth, and by necessity, it will be reduced in its importance, I think.

In current situation there are obviously subfields within mathematics, some of them quite obscure, some of them are obscure and then basically later on, maybe decades later, become important. In this world of specialization, how do you think that is changing when I can either push my ideas into the general understanding or vice versa, I basically can pull from these fields of specialization? How do you see this happening or this evolving over time?

Yeah, this is a beautiful question. Some there are some really great examples of subfields that sort of grew into importance in ways that they didn't have earlier on. So like some recent examples are like algebraic geometry and and topology, right? Like the they they somehow sort of became central over time in ways that I think weren't

necessarily anticipated when they were undertaken earlier on. I I really don't know how this is going to play out. this is quite tricky in in many ways, right? In part because one of the features of

Formalized mathematics is that in principle you can think about it at multiple levels of abstraction. And so there might be sort of ways of moving up and down the abstraction ladder from specific results to sort of more abstract general results more quickly. A counterpoint is that you know a lot of the ways in which we do mathematics at the frontier depend on.

Definitional structures, especially, but also other things that are very particular to the area of mathematics in which we're working. So there's no obvious impediment to AI sort of surmounting that translation between subfields, but it's not merely a question of like going up and down at an abstraction level, right? Like it can there's a lot of translation questions that would also have to be answered along the way. And and and sometimes those kinds of things and

It's not always easy to keep the essence of what's important about an argument as you move.

one context to another.

to finish a bit on this topic, you've covered multiple criteria that can make math valued. While you talked about hardness, talk about the demand in sense of practical application. I think intuitively we all imagine what kind of demand could come from industry, from physics and so on. But for the kind of niche topic that Philippe just alluded to, topics which started as niche, I guess he...

the origin there, it was really driven by kind of the interest of some mathematician who didn't necessarily care too much about the industrial application of them. I guess I'm just curious, what's your mental model on what can make humans so good today at this? What is the kind of property humans have that makes them interested in those questions before the interest is obvious, the application is obvious?

And is this something AI can somehow mimic or is this kind of a gap between the two flavors of intelligence?

so one of the things that people often say when they're talking about abstractions or lemmas is usually the way it's sort of glossed, but it could be anything, definitions, whatever. you know, they talk about generality, of course, have already mentioned this, reusability, but there's also this notion of naturalness. And like, you know, I mean, what does it mean? I think is a great question, but like, you know, somehow it means something like, well.

A lemma is beautiful if it's, you know, somehow easy to state and and prove.

Mmm.

Right? So if it's long and complicated and detailed and gets reused, that's one thing. But if it's like simple and elegant and reusable all over, that somehow is is is nice. but yeah, I think this question of naturalness really is is the thing that jumps to my mind.

And I'd love to try and actually tease that even more if we can. I know for instance in physics, there is some kind of general criteria of symmetry of an equation is supposed to be, make it more pretty and actually just being a short equation obviously, looks better on the t-shirts if you want to Einstein equation.

Mm-hmm.

Would you say math is similar to physics in the sense of kind of the aesthetics that would guide the...

interest in a specific property or another, or is this really something specific to mathematics?

Yeah, I mean I think the you know, for sure that's true, right? Like symmetries and things like this are very mathematical objects as well. I think

You know, one of the interesting parts is about math, especially, I mean it holds for physics too, but you're constrained by the world. But in mathematics, right, like you get to state the language, you get to decide on the language in which you're talking about things. Right? and so, you know, depending on your choice of language, those symmetries may or may not be sort of obvious or manifest. And

Interesting.

so so I think there's this sort of interesting sort of

You know, a person who frames the question in the right way is often the person who sort of observes the the, you know, key beautiful insight. right. We often think about math pro problems as being like, just intrinsically hard, but I think that's not quite true. Right? Like I think there's the way it's stated and it's the way you think about it.

the language that you have to express it. And like oftentimes breakthroughs come from re-expressing ideas in slightly different ways.

And maybe again, this world naturalness, because I like it so much, is the implication that the beautiful math results should be surprising or unsurprising?

Yeah, I mean I think, you know, surprising results certainly like have a particular value. but also right like as we've discussed before, right? If it was just hard to prove, even if we kinda know what you know the answer is, or if we have like a very strong bet, that that has its own value. And so, you know, the the economy of mathematics, if you will, is

In the overall community of mathematicians, looking in from the outside, my feeling is there is also opposition to this idea, or sometimes very harsh. Can you maybe, for us or for the audience, try to steelman the argument from the other side? Why not to follow this route? Why the human will be central, et cetera? I mean, there are a couple of arguments, but pick the one you...

you find most interesting and you want to try to steelman.

Yeah.

I think mathematics is interesting because more than any other discipline, it's really three things, right? It's a discipline, of course. It's a subject matter that we we learn. It's also a practice, and it's the practice of being able to produce correct proof.

But it's also a culture. And that culture is the thing that gives rise to the other two somehow. Right? Like we've we students, when they are doing PhDs, are indoctrinated into this culture that has certain kinds of standards, that has certain ways of thinking, that has certain values. that

I think is important to mathematics. And I think, you know, one big piece that people don't often talk about necessarily of of why people are opposed is that, you know, some aspects of that culture are gonna change. and

And I think there's a sense of loss there that I think is very real and and understandable.

There are lots of other arguments that people also make, but I think that one is is a particularly of interest to me because among among the sciences, you know, to the extent you think of math as a science anyway, mathematics has been able to accumulate knowledge in a way that's really fundamentally different. it's just been able to advance so far and so reliably, right?

You you just don't have situations where whole fields of mathematics collapse. Even though they're like gigantic towers essentially of arguments built on top of each other. And I think it's a great achievement of humankind to to be able to do this and sustain it over generations.

As an economist, also economists use quite a lot of math. And for me, there is like for many other people, I think that are not mathematicians who use mathematics. There is also this outside question. I mean, this sounds like a fantastic opportunity for the rest outside of mathematics. Right.

Yeah.

Can you give a bit your perspective on this as well? Like how you see the leverage there and what are the, what are the most obvious, maybe the low hanging fruits as well in the near term?

Yeah, there's a you know it's often said that mathematics is the language of science. But when you actually look at how that works out, right, like it's a very tenuous relationship at best.

Yes.

we we use mathematics for sure, but it looks nothing like pure mathematics for the most part, with a few subfields like

you know, maybe exceptions, right? Physics, theoretical computer science, places where economics touches theoretical computer science, and you know, those kinds of places where there have been there has been some crosstalk with mathematics, but you know, there are huge areas of science that have, you know, very little to almost no like rigorous to a mathematical standard theory.

And you know, partly because it's hard, right? Like I'm not saying like we we would we should have this like immediately, but partly because the incentive structure is very, very poor, right? Like mathematicians who know math could in theory go over to other fields and try to help them out by proving things. This has been done famously by many, von Neumann being a good good example.

I was just about to

say, and that by besides having a role in the war and just

Yeah. Right scale button. Yeah.

doing something on the side, essentially revolutionizing economics. Yeah, exactly.

Yeah.

but there are others as well who have done similar who have tried similar things. but

But that, you know, even even if you wanted to do that, most of the time the theories in those fields are wrong, right? Like that's kind of the point is they're they need to be sort

Mm.

of improved over time. And so, you know, if mathematicians were to go over there and prove big theorems there's no obvious sense in which they're definitely going to be relevant in ten years. And so given the difficulty of doing mathematics at all, right, like it the incentive structure is just bad, right? Like why why why would one do that with one's career?

It's not that it hasn't been done historically and actually quite fruitfully in some interesting cases, but but the science actually turned out to be wrong. which, you know, is kind of the way science proceeds, right? Like it's just you know a fact. And so there's sort of a a situation, and that's where we've been for you know decades and decades, centuries even. and I think what's really exciting here is that you know, now it's gonna be possible for

scientists to actually use mathematics, at least in theory, right? So in in lots of fields of of science, especially physics, you talk about inverse problems, right? So you wanna you have some model, you observe some data, you wanna infer the parameters of that model.

That's very standard way of operating with you know computers these days. In principle, when math is formalized, you could ask if you could do something like inverse problems to theories themselves. So, what are the mathematical

Mm-hmm.

laws that this domain obeys? And we don't have lots of examples of what this might look like necessarily. Symmetries are sort of the closest example in in physics, but like

You know, i it's the kind of thing that you could try. and and you wouldn't need necessarily the full power of, you know, a graduate degree in mathematics in order to pull it off, right? You have to be able to write statements in in mathematics, theorems that are, you know, potentially true.

But it the and interpret them, right? Like but you don't have to do the whole proof process necessarily, right? If the AI tools are good enough anyway, which, you know, it seems

It

also seems like the search of the right tools becomes actually more important in that case than the full depth basically.

Yeah. So I think this is really exciting, right? I think this applies to software

Yeah.

and physics and economics and you know, potentially further flung fields like chemistry and and biology and and others.

Yes.

Maybe

to link back again to culture, I guess. So obviously the profession of doing mathematics is going to change like many are going to change with the AI revolution. And there's an aspect of loss in the sense of habits that we were attached to. I suspect there's something also kind of objectively fun or not fun about certain aspects of mathematics. I wonder what...

What do you think is the balance? Like what are we losing? What are we gaining in terms of what's actually enjoyable in the, in being a mathematician?

Yeah, I mean I think

we'll lose certain portions of that culture that were n necessary to sort of produce reliable proofs. and like it's hard to enumerate exactly what parts those are, but you know, there's

You're

inting at like some sort of rigor or scientific method or...

It it it's the rigor, but it's the process that leads to the rigorous result. Right. And that's why it's hard to sort of put a a specific finger on, because it's that whole process of education that you go through, you know, where you've done something very, very hard and along the way it was no fun. But when you look back on it, you're like, wow, that was really great.

Yeah, it gives meaning.

Yeah.

And and so that that I think is going to change. I think there are a variety of other changes that or things that are that will persist, right? It will still be important, right? The computer can't understand for us. So we'll still want to understand arguments. Why is a thing true? Not just that it is true, right? Like

a real deep understanding. And you know, for this reason, right, in mathematics, it's totally accepted and desirable in some context to have multiple proofs of the same result. Right? Well why? Because we care how things are true. Like what are the conditions under which it is true.

And I think that that will be preserved, right? That work still has to be done by humans. And it's and it's fun, right? Like that is, you know, that is the learning that we wish to have. the aha will like of of actually like getting to the end of the result, right? Like maybe that's a little bit diminished, but I I don't think that's the hugest part. I think another thing that will be important about mathematics is

So informalized there's this really interesting phenomenon which mathematicians know, but like doesn't really it's not really in your face every day, which is that if you read a mathematics paper in a journal, they omit all kinds of details. and

You know, this varies by subfield, but you know, sometimes by author and so forth, but like they all pretty much omit details because it would be so tedious to write down

Mm.

everything in every step. formal verification languages require that you do that, that that you have every step. and so there's this gap between informal mathematics, the way we practice it today, and formal mathematics.

and I think that's interesting in and of itself, right? It's a there are a couple things, like one question is like what can be omitted? And that depends on the audience.

Hmm.

Right. So if it's another mathematician

Alright.

in the subfield, which is more or less what papers assume now, then like that's one thing. if it's a student, well, you could get a more detailed version of that. Like there's this sort of like interactivity there that's potentially important. So there's this sort of communicative aspect that I think is is clear when you look at the contrast between formal and and informal math. That

That I think, you know, for now anyway, humans are still sort of the arbiters of. Another feature is that we often like move, we reorder the argument.

Mm-hmm.

So if you look at formalized mathematics, it's a directed graph. And so you can just produce a graph of nodes point with arrows pointing, and the theorem that you care about is at the bottom. The definitions that you're depending on are more or less at the top. There you go. But like if you look at a paper, right, you pull the sort of core of the argument to the front.

Hmm.

or what's interesting and important, whatever the contribution is of of the work. and so there's this all this manipulation of the underlying logical structure that we do that I think, you know, at least for now is still work that we need to do.

Can I maybe touch on the, I guess the question of creativity, because it also relates to fun, right? I don't know, from my personal experience, what I remember being part of the fun in mathematics was this freedom of creating world, creating assumptions, creating situation for yourself, and then immersing yourself into that world, seeing what happens. There's almost an aspect of travel and this playfulness, I guess, was fun.

But what I worry bit about is if mathematics become much more of a formally verified science, that maybe, again, you had to do it already many times, but maybe we're going to move from a culture where a lot of the time is spent on the kind of creative work to where the more, I don't know, analytical work maybe.

Mm-hmm.

Did you think that's a possibility or would mathematicians just prefer to spend more of their time on the creative side and just kind of stick to it?

because that's what they want to do.

Yeah, I mean I think

I think there's a couple things to say. Like one is that formal verification of

Well, auto formalization, I'll start from auto formalization, right? Like

Mm.

you're assuming that you've already got a paper and you're gonna translate it into a formal verification language. Still,

Okay.

like not not to belittle the problem, it's still hard and and important, but like you you're at the end of the math somehow. and formal verification works that way most of the time, right? Like it's hard to think of examples in my experience, and I've talked with others who share sort of similar experience where

Where the essence of your argument came from actually doing something precisely formal. Right? It's often like out of board where you're glossing over a variety of details and you know thinking a little bit less rigorously somehow. And so I think.

I think that is what mathematics is most of the time, up until that last mile, where you're actually like writing down the gory details of the proof. And I think people will spend more of their time in that front space. And I think that's that will potentially be quite good. Right. And the reason why I say this is because there are there are relatively well-known examples where

Fields that aren't mathematics that allow more informal argumentation, like physics, have made advances that took many years to sort out in mathematics. Renormalization theory is one well-known example. But there are others where being able to operate at a slightly less rigorous level has demonstrably allowed them to produce results that were just not accessible from mathematics.

at the time they were created.

I see. I wonder, there's an analogy I wanted to test with you. Maybe it's just, maybe the two things are too different to really be comparable, but I know in the world of chess, something that has changed really drastically in the last few years, actually chess has boomed during the COVID break, right? You know, it has become a much bigger sport than it used to be. But there's one really fundamental change now, which is that people say the game is less creative in the sense that

A lot of the moves that people are playing now are things they've learned from algorithms. Basically like an algorithm has learned that, you know, this situation is good to do this. And humans don't even really know why necessarily they treat it more as a kind of a black box. And imagine something similar could happen in math where sometimes you just need a lemma somewhere. You just get chat GPT to figure it out for you. And maybe you don't even try to understand it because it's beyond what a human could do. Right. Like in chess, the very often these computer moves that are really beyond the kind of human.

understanding, right? Do you think is there a possibility that a similar path might happen in math?

I mean, such things are surely possible and they'll happen in some places. but I feel like in mathematics it's, you know, it's less likely to happen precisely because so much of math is about what goes beyond just knowing whether something's true or not.

in there is a sort of like can we get a proof of you know name your favorite famous result but if you look at the examples that have happened historically such as there's a proof of the four color theorem that was done by computer and it's famously inscrutable

Mm-hmm, that's right.

and you know I don't

I don't think it prevents people from thinking about the four-color theorem if they're so motivated, right? Like if we had a different proof, that would be fine. and a useful contribution. and I don't think anyone

I don't hear a lot of positive things said about that result necessarily. Not not you know, I think it just doesn't meet the sort of criteria of mathematics

You

Interesting. Yeah, Yeah.

that we practice today at least, right? and it's totally possible these things will change and relax. but I kind of hope they don't, right? that's one of the beauties of mathematics and mathematical culture is that there's a real standard around understanding.

Excellent.

Patrick, we have already taken up lot of your time. Maybe closing by actually turning back to your initial statement that you are interested in learning. Learning will change broadly, not only in mathematics. What is your view on students and how students will learn in five years?

I think this is a fantastic question. at the graduate level.

it's gonna I think look quite different. right, and this is precisely because so much of the graduate level work in mathematics is about, you know, training someone to produce a proof to a standard of their literature that other researchers in that area would accept. and and so you need a feedback signal in order to make that so.

And that's your advisor, usually, and other you know, students in your area, et cetera, papers that exist. but it's easy to imagine a world, you know, not very far down the road where you can interact with an AI agent that can do that for you. Right? There you can get your sort of reps and sets improving things through an infinite set of problems.

a potentially infinite set of problems anyway.

And getting that fine-grained feedback. And so, like that kind of training, I think, well, it won't just be available through your advisor primarily. and so you know, that that part of education will change somewhat. my hope is more of mathematics will be pushed down toward the lower levels of education.

Historically, it wasn't that long ago where more of mathematics was covered by in for more students at a younger age. You can look back in scientific fields, like some of them were more rigorous at various times and have sort of drifted away from that. but also you know, just in in education itself. And so my hope is that this will help.

help push that back in that direction. Obviously there are other things going on at that in those times that you know not everyone got educated. You know, lots of caveats here and and sort of complexities.

Yeah.

But you know

Making rigorous mathematical training more broadly available is I think one potential amazing win of this process. Not everyone's gonna have a mathematician that they can talk to, but you could

Hmm.

have an AI that is pretty good. And that I think would be great.

Awesome. Patrick, thanks a lot for being part of this.

All right, thanks.

Thanks so much.

Thanks for watching. We have got more episodes in the oven, so please like and subscribe to get notified when they are out. And please check out taste-bench.com to read about the taste benchmarks and the creative engine we are building towards.