The frontier of math is too vast to be understood. Research is necessarily becoming more and more specialized. There are more mathematicians than ever, but most published research is going essentially unread (my claim). Most (all?) of our professors at Colby were in niche fields maybe with less than a dozen active contributors.
Meanwhile axioms are being codified and programs are being used to generate proofs (see the four color theorem). These proofs are (and especially will be) incomprehensible to us. Proof-checking will be a job for computer scientist, not traditional mathematicians (really, of course, one must be both).
So what is the future of mathematics?
Will research continue fractally in every direction for the indefinite future? More and more complicated and esoteric, but never ending?
Will it always be a job fit for humans? Or at least some?
Will computers never (for the foreseeable future) be able to create new fields of math, presumably requiring great creativity and unconstrained thinking? Will they just be tools to proof what we are interested in?
Will we simply ignore the never-ending proofs generated by computers for a lack of interest?
Will math become the math of our college careers, not of our professors? Solving problems for fun, not for publication.
Idk they might be able to get there and contribute something. I know hardly enough about computers to make an informed response about this.
By ignore do you mean act as if they don’t count, or ignore reading them and take them as true? The former seems more likely for mathematicians, the latter physicists will be cool with.
I don’t think so. That would be cool but my Iowa experience leads me very pessimistic about that possibility panning out.
I’m not sure if this means all that much for physics. There will continue to be mathematicians whose niche is motivated by physics, and physicists who draw from such math for inspiration. I guess more types of math may get overlooked by physicists simply because there’s more out there. Physicists will be more accepting of computer-proofs than mathematicians I think.
Probably. I like to hope that “unifying projects” similar to the Langlands program will come and try to bridge these separate branches. I suspect this gets harder to do as time goes as you need to specialize in at least two of these highly specialized fields and still have left over brain to see the connections.
Always? Probably not. For the foreseeable future? Probably.
I suspect this is reliant on the creation of agi; granted as someone working in mathematics my ego rests on this being the case but I fail to see how the systems we build now would ever be able to do it. As for timeline, I don’t know if agi will ever happen so I guess for the foreseeable future sounds good to me.
I don’t think anyone cares that they were generated by computers. The proofs are simply ugly, hard to understand, and don’t seem to be very enlightening. So until computers can generate more human consumable proofs, yeah the math community will probably continue to be uninterested.
I would love for this to be the case, but right now my advisor is basically saying “this problem is interesting because I think [insert prestigious journal name here] would publish it”. Also so long as how tenure track professors are picked involves some level of “how much have they published” it will probably fail to improve much. Maybe we need to revolt.
I don’t know the first thing about physics, so I leave it to others to speculate on physics. For any field on the outside looking to use the mathematical theory it probably makes it harder to grok what may be useful. According to a couple of conversations this seems to be happening in geometry processing at the moment: the community is lagging about 100 years behind the pure geometry world and are really struggling to work out which constructs are useful to use and which are just… pure mathematician noise.
Interesting. I’ve actually never heard of this. I’m only tangentially aware of category theory as well, but I guess that’s moving in the same direction.
I’m imagining a (near?) future in which you simply encode (almost) any problem and have a computer prove it true, false, independent, or so difficult to prove so as to be reasonably considered out of reach. Perhaps this last status leaves some room for human innovation. But anyway, it’s conceivable that anything you might want to prove could be done faster by a computer than a mathematician.
So what might happen when the pace of this more “observational” math far outpaces that of traditional proof writing? Will mathematics become a field of setting up structures and problems rather than solving them? Or will the focus and goal of mathematics shift from proving theorems to seeking logical beauty? Probably both and there will be a bitter divide.
But what happens when computers can generate shorter proofs than any human mathematician, possibly even minimal ones? Maybe short doesn’t equate to beauty. But can beauty be codified? If so, we’re done for.
An additional philosophical issue raised by computer-aided proofs is whether they make mathematics into a quasi-empirical science, where the scientific method becomes more important than the application of pure reason in the area of abstract mathematical concepts. This directly relates to the argument within mathematics as to whether mathematics is based on ideas, or “merely” an exercise in formal symbol manipulation. It also raises the question whether, if according to the Platonist view, all possible mathematical objects in some sense “already exist”, whether computer-aided mathematics is an observational science like astronomy, rather than an experimental one like physics or chemistry. This controversy within mathematics is occurring at the same time as questions are being asked in the physics community about whether twenty-first century theoretical physics is becoming too mathematical, and leaving behind its experimental roots.
So it begs the question of what the point of all of this is. If you are a Platonist this will usher in a new age of progress and discovery, or something… Hopefully this is relevant to physics.
But if you aren’t, what are we doing? We’ve picked a set of axioms and are presumably solving problems in the name of fun. Leo (our math professor) remarked once about the good fortune of living in society so rich that it pays for mathematicians to sit around and think (subtext: uselessly). Perhaps when these changes come we’ll all already be out of work anyway. There will still be plenty of time to sit around and think.
The thing with math is it’s so much about getting a personal understanding for why the things you’re studying are the way they are (and then also doing your best to explain it to others), so I could see using the computer this way as a check to make sure you’re not going down rabbit holes, but it seems like just getting a computer to do a proof for you kind of defeats the point in most cases, besides famous super complicated problems that have stumped people for years.
Sure in terms of just number of things proved the observational branch would go way faster, but again as you talked about earlier math is getting so splintered that no one would really care about proving tons of theorems with computers in a field 12 people know exists. Those 12 people would care about the understanding.
I could definitely see there being a sect of observational mathematicians focused on setting up structures and having the computer tell you what’s true or not, but I think there would certainly as you say be a bitter divide.
This scenario seems to be bordering on robots taking over the Earth, in this case I think computers could replace almost any human job, so I’m gonna ignore it cause in that case we have bigger problems. Maybe I’m reaching.
Category theory is, from my understanding, much more about providing a common core language for these fields to communicate with. This would, I suppose, aid in the creation of said unifying projects as now there is more of shared language between them. As a total aside: Applied category theory is increasingly becoming a thing and is kinda neat if you have the time/inclination I suppose.
This divide already exists in a light form with between the applied math and the pure side I think. By the time we hit here I suspect it will come down to “why” you study math. If your goal is purely to get something done, you probably would just switch to mathematicians setting up structures and letting the computer do the grunt work. I mean, the engineering field is already starting to see this where CAD programs will generate geometry for the user given a set of constraints that it must satisfy. ( One of these is called topology optimization and what it produces is really dope looking ) On the other hand if you’re more of the pure bent and you care why something is true then Alan probably hit the nail on the head here:
Any way I don’t see this divide being much more bitter than it is currently between pure and applied math, we give each other shit but I think both respect what the others do. Ok I’ve met some pure people who don’t but I digress.
Maybe, I doubt it. My favorite proofs often have people who disagree with me and think they’re not pretty. There are some proofs that I think are universally accepted as pretty, the infinitude of the primes and irrationality of square root of two come to mind, but outside of these I think even the community at large struggles to agree. Maybe we could do something like the style transfer guys are doing where we could have a statement to prove, a proof whose style we enjoy, and then the algorithm could prove the statement mimicking the style of the other proof.
I tend to stay out of the philosophy discussion so I will here too.
This seems bout right, by the time we have computers doing this we will have probably automated away everything else to do… assuming we didn’t kill our selves to get there. If I haven’t dropped enough things to look into AI safety is another wild thing to read about.
Great post. A lot of things to think about. I’ll definitely look into applied category theory.
I think you’re right on all counts. Realistically, I think computer generated proofs will continue to be brute-force and difficult to apply for the foreseeable future. That will keep them relegated to a certain type of mathematician as it is now. It may not invade the rest of mathematics for some time (some might think never).
Perhaps a machine which can prove general problems as I’m describing above will inherently be a super intelligence in many of the ways we think of it, even if not yet fully practical. So we can wonder whether or not we can create such a machine before AGI, if AGI is a prerequisite, or if the two are equivalent.
