yesterday at 10:00 PM
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
yesterday at 10:56 PM
> 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.
yesterday at 10:38 PM
> 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.
yesterday at 11:09 PM
> 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.
yesterday at 9:09 PM
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.
yesterday at 9:23 PM
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).
today at 12:06 AM
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.
today at 12:13 AM
How do you handle the 'people often learn through repetition' problem?
yesterday at 9:45 PM
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.
yesterday at 9:28 PM
> If the aim of mathematics is to promote greater human understanding...
Is this the aim of mathematics?
yesterday at 9:51 PM
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.
yesterday at 10:45 PM
> 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.
today at 12:15 AM
The irony is his words just became AI training data to immortalize becoming useful through the point you just made.
yesterday at 11:36 PM
Did any mathematics done by G H Hardy turn out to be quite useful in the end?
Ironically of course the answer is yes.
yesterday at 10:48 PM
Even if it were not, it is a wise aim, unlike ceding understanding to a robot.
yesterday at 9:36 PM
This is certainly what many mathematicians have used as justification for why humans should continue studying math.
yesterday at 11:13 PM
> 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.
yesterday at 8:54 PM
>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.
yesterday at 9:50 PM
>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.
yesterday at 10:12 PM
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.
yesterday at 11:07 PM
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.
yesterday at 10:47 PM
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?
yesterday at 9:12 PM
> 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?
yesterday at 9:48 PM
Important to the field of mathematics.
yesterday at 10:00 PM
"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.
yesterday at 11:18 PM
>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.
yesterday at 9:38 PM
> 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.
yesterday at 9:16 PM
> 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)?
yesterday at 9:09 PM
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?
yesterday at 9:20 PM
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?
yesterday at 10:15 PM
...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?
yesterday at 8:59 PM
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.
yesterday at 8:52 PM
[flagged]
yesterday at 9:01 PM
> [mathematics] being funded by a small number of rich [people]
Historically this has always been the case. Rich people or people supported by rich people did math, while peasants worked the fields and workers worked in factories/mines/etc. This is just regression toward the mean.
yesterday at 9:20 PM
Historically life was a lot worse.
yesterday at 9:31 PM
>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.
yesterday at 10:02 PM
That will also happen with regulation. It's just gonna be slightly slower process
yesterday at 9:34 PM
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.
yesterday at 9:38 PM
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
yesterday at 10:55 PM
> 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"
yesterday at 9:38 PM
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.
yesterday at 10:54 PM
> 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.
yesterday at 11:26 PM
> 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...