The Future of Mathematics(terrytao.wordpress.com) |
The Future of Mathematics(terrytao.wordpress.com) |
I doubt of this progress could have been made without the specific combination of Lean + Mathlib. Automatic Theorem Provers are not a new idea, but we don't see these breakthroughs happening with any other stack
For sure math and software people know this, as it's kind of hard to ignore. Developers who are totally disinterested in nerdy stuff like theorem proving will very quickly hit a wall without letting their models indulge in test suites (regardless of whether they ever even glance at the tests themselves). Physics nerds get it, and if they are on more on the experimental side then they are working to give it some kind of sandbox, all the other science wonks are getting it or will get it as they work with their more computationally inclined colleagues, same for general engineering.
There's a real danger here though in that there is no reason the general public will ever become very much acquainted with the verification/validation steps that all these systems actually need to be reliable. They just hear about this or that nearly impossible thing finally being accomplished as if by magic, and they won't do the work to think about what's in scope, out of scope, or how anything can be checked iteratively.
Indeed, I don't think anyone should be led to believe that AI can do math on its own without _some_ kind of oracle providing extremely rigorous feedback.
Eh, Lean was heavily developed based on feedback from mathematicians; it's not a side-effect but more like a "driving force."
Source: one of Lean's co-authors.
This is a really uplifting message. I'm currently in school pursuing a degree in applied math, and I've definitely felt unsettled with the recent advancements with automated proving. So it's nice to know that there's still a place for learning mathematics, and that we can find a new way forward.
If the aim of mathematics is to promote greater human understanding, then surely elevating everyone’s grasp and appreciation of math is of greater import than chasing another theorem feather for our hats - especially if AI can automate the plucking.
This keeps being repeated by AI skeptics, yet AI keeps solving more and more complex tasks. We've reached the point that it's even started solving Millennium problems.
>Telling us that some AI agent is spinning out theorems that are highly interesting to it and other AI agents does nothing for us.
This is the future of pushing the frontier though. AIs need to be pushed to get better and better. AI understanding of math is millions times more important than human's.
I'm tired of this cautious optimist talk. It is inevitable that without regulation, AI will eclipse humans in every possible domain, leaving everyone without direct control over the most powerful models completely powerless, economically redundant, and at the mercy of the new AI hegemony. Anything which doesn't confront this possibility honestly is just lying to people.
You could give me the most well crafted, comprehensive document ever and I would still misread bits of it, or miss some crucial bit of information that contextualises the rest or whatever.
With LLMs I can ask endless dumb questions in a way that just would not be practical otherwise. The quality of the responses doesn't even have to be particularly good for it to be extremely useful - it's basically a turbo charged rubber duck for learning new concepts.
I'm experimenting with this at https://miletus.app
I'm also curious about training models with that singular goal. If anyone is exploring similar ideas, I'd love to chat.
Is this the aim of mathematics?
Think of it like this: when your extremely efficient 2-3 SD brain that could pattern match more aggressively than mere mortals seems to be losing ground to aggressively scalable stochastic parrots that can pattern match faster than you, you replace your contempt for teaching and pedagogy with sudden epiphany and awakening that nurturing curious Math lovers and developing the human spirit is what it's all about. It's a good gambit.
This is a persistent misconception that I see on HN (although not usually framed as abrasively as you have chosen to frame it).
Math is not an engineering discipline. Pure mathematics research is not done with an eye towards practical applications in other fields. You should think of it more like the humanities--it is done because it enriches the human experience (and it's not very expensive).
You could give us a black box oracle that could tell us, with 100% certainty, whether the 50 most famous and important open conjectures in math were true or false, and it would be more or less worthless. What does it actually get you? This isn't a rhetorical question.
AI in math is valuable only insofar as it ultimately helps drive human understanding.
There is another side of math that is more driven by practical applications: statistics and "applied math" and whatnot. This is what most people think of when they try to imagine math research, because it is much closer to the math that they have learned in their school education. A lot (but not all) of this math would get more value out of black box results, yes. But don't conflate this with the entire field of mathematics as a whole.
>What does it actually get you?
It gives you truth. It broadens what is known about mathematics.
And now you're hearing it from a guy who's one of the foremost, early proponents of AI in math.
> AI understanding of math is millions times more important than human's.
Important to whom?
Yes, so? Still not "novel ideas and insights", which is what you responded to ... and the statement wasn't made by an AI skeptic.
> This is the future of pushing the frontier though. AIs need to be pushed to get better and better.
It would be far more honest to say "I want AIs to get better and better". But there are costs. What are you willing to accept?
> AI understanding of math is millions times more important than human's.
Ah, it seems that "replace humans with AIs" is not too much for you.
To whom is that more important? Not mathematicians.
Since you’re so certain, how long do you think it’ll be before all of the millennium problems are solved by AI (by leveraging the current literature)?
Math is also a matter of what is both interesting and useful to humans.
For some reason there is this virulent strain of anti-human AI rhetoric that machines will replace us. But what is the purpose of math as a field of study if we're not in the loop?
We make our problems up!
> For some reason there is this virulent strain of anti-human AI rhetoric
It’s just… nasty, isn’t it? Facts aside, one does have to wonder what motivates not the beliefs themselves, but the, well, frankly aggressive, way in which they’re expressed. Bitterness and envy felt towards those who have actually done the hard work and achieved things?
The question is to what extent AI will affect creation of new branches and elegant ideas in mathematics. This question applies to every area. Has it created an interesting new way of thought in any area other than those where massive tree search can be mistaken for such?
I don’t think it’s impossible but the evidence doesn’t point clearly to it.
I disagree. I believe access to AI will shift the power balances of the world, but I wouldn't say people will be left completely powerless. But maybe our definition of powerless differs.
What is your definition of powerless? Unable to influence? Physically outmatched?
> at the mercy of the new AI hegemony
Unless their robot army is fully armed and ready when things get bad enough they'll find out we aren't at their mercy, they are at ours.
England 1381. France 1789. Haiti 1791. Russia 1917. China 1949. World 203X...?
Would be preferable to avoid letting things get to that point by having those in power be smart enough to release the pressure valves as was done in the US around the time of the New Deal, but if they fumble this we shouldn't view being at the mercy of the elites as a foregone conclusion.
Once the average person's base level comfort is gone and they aren't sure where their next 3 meals are coming from anything can happen.
Worth noting that it wasn't "those in power" who decided of their own accord that they needed to improve the situation. It was organized labor, unemployed workers, protests, farmers, and electoral politics.
"Those in power" almost never seem to make such changes of their own accord. They have to be forced. The only question is how much force is necessary.
This reminds me of the early days of Covid: "it's only 10 cases, worry about the flu"
More like The Young Lady's Illustrated Primer [0] than our current chatbot paradigm.
I expect there are 48956789560984 startups trying for this now, though, so... soon?
True, the populace drove the change and would have seen things changed by whatever means necessary.
My point (about "those in power") was that at least FDR was smart enough to know this and realize the least disruptive way forward was to convince the business interests to suck it up and save the capitalism that benefited (and would still benefit) them by introducing a bit of socialism to avoid complete chaos.
There appears to be zero appetite for that sort of compromise with our current administration or our current business leaders who are still clinging to failed neoliberal trickle-down ideology, though you can see the people clearly shifting fast in recent elections.
I'd like to hope that this change in attitude continues to bubble up to the political levels required in time to avoid the more extreme outcomes, but I guess we'll see...
There's no such consensus. Read Hardy's "A Mathematician's Apology" to get a better understanding.
Here's a quote which gives some idea of where Hardy was coming from: "I have never done anything 'useful'. No discovery of mine has made, or is likely to make, directly or indirectly, for good or ill, the least difference to the amenity of the world."
Hardy valued math for its beauty, elegance, and permanence, and he's far from the only mathematician who would push back on the idea that mathematics should be "useful to humanity", except perhaps in the sense that art is useful to humanity.
Ironically of course the answer is yes.
It's also very risky to frame it that way, because that immediately leads to the idea that mathematical endeavors should be judged and funded according to their expected utility. That's product development, not research.
It seems to me that it would be cool if that could be solved automatically for any learning goal/target
It's def not as robust as Math Academy's graph yet, they spent years hand-building and testing it on real students. But I bet a few more iterations of frontier models get there, especially once there's learner data to correct it.
We do math mostly for fun.
If humans didn't exist do you think a^2 + b^2 = c^2 would cease to be a thing? Math is built on top of logic and it is something that exists independent from the physical realm.
Which gets closer to my real point, mathematics is inherently philosophical and I’d argue it is a kind of analytic philosophy. A close reading of late 19th/early 20th-century history of mathematics, I believe, shows us how closely mathematics developed alongside analytic philosophy, such that at the foundational level at least, they seem to be the same branch of knowledge. It wasn’t too long ago that in some parts of the world mathematics was (rightfully in my opinion) considered a branch of philosophy and there was no clear separation between a philosopher and a mathematician. So, in my mind, mathematics is the way it is, or is beneficial to humans because, or is worth pursuing ourselves instead of handing most of it to machines because of the same reason as philosophy is all of these things: human beings are naturally curious and we satisfy our curiosity by trying to learn and understand things, it’s a natural drive and it’s among the things which help us grow as individuals and as a collective.
Personally, I consider the above a very practical value, so I’d argue that pure mathematics does have “applied” value at a more basic level than what engineering or science disciplines are usually concerned with.
Bureaucracy has no direct value, but it may have indirect value, if it helps us achieve things that are more directly useful. Pure mathematics has had a lot of indirect value until now. It turns out that training people to do mathematics for the sake of doing mathematics, at any level from schoolkid to mathematics professor, teaches skills that transfer to other domains. If human thinking becomes obsolete, that indirect value may be gone, but the direct value will remain.
The results in pure mathematics are largely irrelevant, except as means of acquiring transferable skills. Sometimes they have practical implications, but such situations are exceptional. And there is not much correlation between the practical value of a result and its value as seen by mathematicians.
Why does anything have value? Ultimately because we can use them to get something we need or want. For the former, there is some sense in trying to reach an objective definition of value. The latter is inherently subjective. Some things are valuable to some people, because those people find those things valuable. That circular definition is the root of subjective value that cannot be reduced any further.
If you disagree (as the GP does, apparently), I ask you--what value do you see in it?
He simply said what pure mathematics is. You brought the "ought" part in. By what standard do you determine what pure mathematics ought to be good for?