I think too much credit in the AI math discussion is being given to LLMs rather than to Lean, which an incredibly well designed language around which Mathlib coalesced as a side-effect of it's capability
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
> I think too much credit in the AI math discussion is being given to LLMs rather than to Lean,
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.
I am not really sure. The models can be bootstrapped to become much better at both natural language generation and verification for sure and my hypothesis is that the current days models would have been just as good at math without Lean.
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.
Not sure why you say that. All the major AI-generated proofs so far were done by AI without using lean, and then later validated by AI formalizing with lean in a separate process. Do you mean we would not have enough rigorous training data perhaps?
Relatedly, I think where I land is that the (current) challenge for humans is creating such oracles. AIs have patience and compute we can only dream of—I think someone estimated 100,000 person-years were spent on Navier-Stokes—but they still need a “reality” to measure against.
> Despite the uncertainty, there are some clear messages we can send to the next generation of mathematicians. The first is that we stand with you. ...Second, mathematics is as important today as it ever was, and we need you. AI must not replace our collective ability to reason and deliberate, and mathematics remains a core capacity for doing so. We cannot imagine a world in which mathematics does not play an important part in our lives.
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.
It’s easy to get caught up in the worldview of academia, where the value of mathematics can seem tied to producing new interesting proofs... I’m a mathematics teacher, and I’d remind you that wider society really values people who are good at mathematics, even if they never prove anything groundbreaking. The ability to reason mathematically is useful far beyond the bubble of mathematical research. There will always be a place for mathematics grads so don't be discouraged by the AI news.
It really depends why wider society values people who are good at maths though. Unlike the arts, society (in my view) values people who are good at maths for purely utilitarian reasons; up until now strong mathematicians have been neccessary to meet various end goals. There's a very real risk that LLMs (or AI in general) will in the near term future surpass humans in all of those pursuits.
Maybe the next frontier for AI is to make it more pedagogical.
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.
Arguably it is succeeding on this front - LLMs have been much more helpful for learning about mathematics topics than Wikipedia for a while now. Admittedly a somewhat low bar, but they are genuinely helpful. In many other fields the models can still only pull up equal (in my opinion).
It's the 'can answer arbitrary questions' part for me.
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.
Agreed. An always-on agent focused solely on improving your knowledge/skills could ask you questions daily, build a picture of the gaps in your understanding and learn where to push you next.
I started with a curated backbone across several fields, drafted with frontier models and reviewed by hand. The automatic (and fun) part happens when you pick a goal and a quest gets generated with its own prerequisites, mapped onto that backbone.
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.
The aim is to produce a body of knowledge that will be useful to humanity. So far, the best way to ensure that knowledge is useful is to have a society of experts who understand them well. That may not be necessary any more with AI, but it's a scary thought -- because that logic can be applied to any human knowledge, not just mathematical.
> The aim is to produce a body of knowledge that will be useful to humanity.
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.
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.
>Can every interesting mathematical question be answered that way? Probably not, and even questions that can may have more interesting and satisfying solutions that invoke novel ideas and insights. Perhaps, in the near future, AI systems will be able to come up with such insights, but, at the very least, let’s recognize that we are not there yet.
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.
>AI understanding of math is millions times more important than human's.
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.
But why? Responding to vulgar economism/instrumentalism with, "Well actually mathematics is this and that, human understanding/journey etc. etc." does not explain why mathematics ought to be those ways. Without elaboration such assertions amount to professional dogmatic narrative in the other direction. Professionals can be very good at that kind of rationalization too.
When mathematicians speak of pure mathematics having “intrinsic value” or being for the sake of improving human understanding, what they really mean is that no applied value (in engineering or science usually) is necessarily known at present, but it improves our understanding of mathematics as a system in itself. Why mathematics is this way is not an easy answer, you would have to first have an agreed upon definition of what mathematics actually is, and we don’t have this. Most people have an intuitive notion and “know it when they see it,” but mathematicians and philosophers of mathematics don’t have a clear answer, and different schools like the (neo-)platonists, formalists, constructivists, etc. have different contradictory approaches in even trying to get to a clear definition.
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.
Some things are valuable, because they keep people alive and healthy in the short term. Some are valueble, because some people find them inherently valuable. Pure mathematics is in that category. And then there is bureaucracy.
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.
See we're taking about inherent value but part of that is my valuing a not nonsensical explanation. And saying math has intrinsic value because some of us treat it as that is nonsensical and anti-science or anti philosophy. It is not based on an intelligible definition of value. Which goes to my original point that when people trot out these arguments they are really thinking carefully about what they are saying. And the more you see these talking points repeated I have to ask who is putting forth these notions. And so every time it is someone making these sweeping declarations about "value" and other people are supposed to accept that. It is a kind of ideological being talked-down to, what gave them the position to declare the ontology of value and so forth. And that is pattern once pointed out you'll see people keep doing it.
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.
I think I already answered this in my comment. I claimed that I don't see much value in a magical black box theorem-proving oracle whose proofs could not, and would not, be understood by humans.
If you disagree (as the GP does, apparently), I ask you--what value do you see in it?
You claimed it would be worthless but did not give any supporting rationale for that claim. That is the ideological move. Professionals are often blind to this.
> does not explain why mathematics ought to be those ways.
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?
"The field of mathematics" is something that humans engage in, chiefly to advance human understanding in about the most abstract way possible. It's not some self-sufficient, sentient being that exists for its own sake. Also, contrary to what's often repeated by AI maximalists, it's not a major source of innovation in other disciplines; most of the math the world actually runs on is hundreds of years old.
>It's not some self-sufficient, sentient being that exists for its own sake
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.
> 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.
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.
Math as a field is unbounded. There's always more to discover, new systems to invent, new problems to find. It's not just some predefined set of unsolved problems.
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?
It’s like people think problems are given to us by God.
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?
...but math does have applications! maybe there is some math that people can't understand, but which has engineering applications, and which machines might apply to solve problems?
Tasks are not simply integer “difficulties” where, if your “intelligence” exceeds the “difficulty” then you will solve it.
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.
>Finally, the next few years will be extremely interesting. We are at a new frontier, where our communal norms, values, and expectations are beginning to break down, and it’s up to all of us to figure out what should replace them
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.
> 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
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?
A lot of people are tired of a lot of talk. It's not going to get anywhere if they all just consider the other views as only possibly held by liars instead of something to discuss and reason about.
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.
> those in power be smart enough to release the pressure valves as was done in the US around the time of the New Deal
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.
> 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.
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...
Yes people have broken down the norms, but AI isn't eclipsing anything. AI itself is a human achievement. By my count AI contributions to society are still 0.00000001% of human contributions to society, and it's not catching up since once of its main effects on humans is to make them antisocial. The reason I'm not freaking out is that it's the AI users who are destroying themselves. The more you buy into the lie of an AI future, the more it is you being sucked dry. I just don't have the energy to save people that don't want to saved, and LLM users and gambling addicts fall in this category for exactly the same reasons
I think too much credit in the AI math discussion is being given to LLMs rather than to Lean, which an incredibly well designed language around which Mathlib coalesced as a side-effect of it's capability
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
> I think too much credit in the AI math discussion is being given to LLMs rather than to Lean,
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.
I am not really sure. The models can be bootstrapped to become much better at both natural language generation and verification for sure and my hypothesis is that the current days models would have been just as good at math without Lean.
> rather than to Lean
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.
Not sure why you say that. All the major AI-generated proofs so far were done by AI without using lean, and then later validated by AI formalizing with lean in a separate process. Do you mean we would not have enough rigorous training data perhaps?
Not just feedback, Lean provides validation as well.
Relatedly, I think where I land is that the (current) challenge for humans is creating such oracles. AIs have patience and compute we can only dream of—I think someone estimated 100,000 person-years were spent on Navier-Stokes—but they still need a “reality” to measure against.
> which Mathlib coalesced as a side-effect of it's capability
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.
> Despite the uncertainty, there are some clear messages we can send to the next generation of mathematicians. The first is that we stand with you. ...Second, mathematics is as important today as it ever was, and we need you. AI must not replace our collective ability to reason and deliberate, and mathematics remains a core capacity for doing so. We cannot imagine a world in which mathematics does not play an important part in our lives.
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.
It’s easy to get caught up in the worldview of academia, where the value of mathematics can seem tied to producing new interesting proofs... I’m a mathematics teacher, and I’d remind you that wider society really values people who are good at mathematics, even if they never prove anything groundbreaking. The ability to reason mathematically is useful far beyond the bubble of mathematical research. There will always be a place for mathematics grads so don't be discouraged by the AI news.
It really depends why wider society values people who are good at maths though. Unlike the arts, society (in my view) values people who are good at maths for purely utilitarian reasons; up until now strong mathematicians have been neccessary to meet various end goals. There's a very real risk that LLMs (or AI in general) will in the near term future surpass humans in all of those pursuits.
Maybe the next frontier for AI is to make it more pedagogical.
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.
Arguably it is succeeding on this front - LLMs have been much more helpful for learning about mathematics topics than Wikipedia for a while now. Admittedly a somewhat low bar, but they are genuinely helpful. In many other fields the models can still only pull up equal (in my opinion).
It's the 'can answer arbitrary questions' part for me.
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 want the multimedia version of this that can animate pictures and play sounds, to help explain things.
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?
[0] https://en.wikipedia.org/wiki/The_Diamond_Age
Agreed. An always-on agent focused solely on improving your knowledge/skills could ask you questions daily, build a picture of the gaps in your understanding and learn where to push you next.
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.
How can you source or generate a curriculum graph (similar to what math academy does)?
It seems to me that it would be cool if that could be solved automatically for any learning goal/target
I started with a curated backbone across several fields, drafted with frontier models and reviewed by hand. The automatic (and fun) part happens when you pick a goal and a quest gets generated with its own prerequisites, mapped onto that backbone.
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.
How do you handle the 'people often learn through repetition' problem?
> If the aim of mathematics is to promote greater human understanding...
Is this the aim of mathematics?
The aim is to produce a body of knowledge that will be useful to humanity. So far, the best way to ensure that knowledge is useful is to have a society of experts who understand them well. That may not be necessary any more with AI, but it's a scary thought -- because that logic can be applied to any human knowledge, not just mathematical.
> The aim is to produce a body of knowledge that will be useful to humanity.
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.
The irony is his words just became AI training data to immortalize becoming useful through the point you just made, which is an asterisk on his name.
Did any mathematics done by G H Hardy turn out to be quite useful in the end?
Ironically of course the answer is yes.
This is certainly what many mathematicians have used as justification for why humans should continue studying math.
Even if it were not, it is a wise aim, unlike ceding understanding to a robot.
> 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.
>Can every interesting mathematical question be answered that way? Probably not, and even questions that can may have more interesting and satisfying solutions that invoke novel ideas and insights. Perhaps, in the near future, AI systems will be able to come up with such insights, but, at the very least, let’s recognize that we are not there yet.
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.
>AI understanding of math is millions times more important than human's.
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.
Where are you getting the applied math angle from. Do you think the recent Navier Stokes proof was applied math?
>What does it actually get you?
It gives you truth. It broadens what is known about mathematics.
But why? Responding to vulgar economism/instrumentalism with, "Well actually mathematics is this and that, human understanding/journey etc. etc." does not explain why mathematics ought to be those ways. Without elaboration such assertions amount to professional dogmatic narrative in the other direction. Professionals can be very good at that kind of rationalization too.
When mathematicians speak of pure mathematics having “intrinsic value” or being for the sake of improving human understanding, what they really mean is that no applied value (in engineering or science usually) is necessarily known at present, but it improves our understanding of mathematics as a system in itself. Why mathematics is this way is not an easy answer, you would have to first have an agreed upon definition of what mathematics actually is, and we don’t have this. Most people have an intuitive notion and “know it when they see it,” but mathematicians and philosophers of mathematics don’t have a clear answer, and different schools like the (neo-)platonists, formalists, constructivists, etc. have different contradictory approaches in even trying to get to a clear definition.
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.
Some things are valuable, because they keep people alive and healthy in the short term. Some are valueble, because some people find them inherently valuable. Pure mathematics is in that category. And then there is bureaucracy.
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.
See we're taking about inherent value but part of that is my valuing a not nonsensical explanation. And saying math has intrinsic value because some of us treat it as that is nonsensical and anti-science or anti philosophy. It is not based on an intelligible definition of value. Which goes to my original point that when people trot out these arguments they are really thinking carefully about what they are saying. And the more you see these talking points repeated I have to ask who is putting forth these notions. And so every time it is someone making these sweeping declarations about "value" and other people are supposed to accept that. It is a kind of ideological being talked-down to, what gave them the position to declare the ontology of value and so forth. And that is pattern once pointed out you'll see people keep doing it.
I don't understand what you are trying to say.
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.
I think I already answered this in my comment. I claimed that I don't see much value in a magical black box theorem-proving oracle whose proofs could not, and would not, be understood by humans.
If you disagree (as the GP does, apparently), I ask you--what value do you see in it?
You claimed it would be worthless but did not give any supporting rationale for that claim. That is the ideological move. Professionals are often blind to this.
> does not explain why mathematics ought to be those ways.
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?
> This keeps being repeated by AI skeptics,
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?
Important to the field of mathematics.
"The field of mathematics" is something that humans engage in, chiefly to advance human understanding in about the most abstract way possible. It's not some self-sufficient, sentient being that exists for its own sake. Also, contrary to what's often repeated by AI maximalists, it's not a major source of innovation in other disciplines; most of the math the world actually runs on is hundreds of years old.
We do math mostly for fun.
>It's not some self-sufficient, sentient being that exists for its own sake
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.
> exists independent from the physical realm
Doubt.
If humans didn't exist, would mathematics cease to have a goal? Yes.
> 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.
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.
> We've reached the point that it's even started solving Millennium problems.
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 as a field is unbounded. There's always more to discover, new systems to invent, new problems to find. It's not just some predefined set of unsolved problems.
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?
It’s like people think problems are given to us by God.
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?
...but math does have applications! maybe there is some math that people can't understand, but which has engineering applications, and which machines might apply to solve problems?
Tasks are not simply integer “difficulties” where, if your “intelligence” exceeds the “difficulty” then you will solve it.
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.
>Finally, the next few years will be extremely interesting. We are at a new frontier, where our communal norms, values, and expectations are beginning to break down, and it’s up to all of us to figure out what should replace them
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.
> 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
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?
That will also happen with regulation. It's just gonna be slightly slower process
A lot of people are tired of a lot of talk. It's not going to get anywhere if they all just consider the other views as only possibly held by liars instead of something to discuss and reason about.
I generally agree with what you're saying, but...
> 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.
> those in power be smart enough to release the pressure valves as was done in the US around the time of the New Deal
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.
> 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.
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...
Yes people have broken down the norms, but AI isn't eclipsing anything. AI itself is a human achievement. By my count AI contributions to society are still 0.00000001% of human contributions to society, and it's not catching up since once of its main effects on humans is to make them antisocial. The reason I'm not freaking out is that it's the AI users who are destroying themselves. The more you buy into the lie of an AI future, the more it is you being sucked dry. I just don't have the energy to save people that don't want to saved, and LLM users and gambling addicts fall in this category for exactly the same reasons
> By my count AI contributions to society are still 0.00000001% of human contributions to society
This reminds me of the early days of Covid: "it's only 10 cases, worry about the flu"
...and humanity is still here. It seems pretty resiliant.