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
j2kun 24 hours ago [-]
> 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.
pama 20 hours ago [-]
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?
j2kun 6 hours ago [-]
> All the major AI-generated proofs so far were done by AI without using lean
Is that true? I was under the impression they used lean as they went.
famouswaffles 4 hours ago [-]
Yes that is the case. DeepMind's AlphaProof/Geometry that won IMO Silver used lean as an intrinsic part of the process 2 years ago, but things have shifted. When DeepMind and OpenAI won IMO Gold a year ago, it was solved end to end in language and translated to lean afterwards, and that has been the case since.
7734128 18 hours ago [-]
Because the RLVR probably uses formalization to judge rollouts.
singularity2001 16 hours ago [-]
because LLMS are like drunk geniuses, without the rigor of lean they would drift into nonsense. Similar in chess they have 1700 ELO now but still some percent of their moves are illegal.
chorsestudios 20 hours ago [-]
Not just feedback, Lean provides validation as well.
ianjbutler 20 hours ago [-]
> 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.
afthonos 22 hours ago [-]
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.
SmartestUnknown 19 hours ago [-]
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.
erichocean 24 hours ago [-]
> 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.
smj-edison 23 hours ago [-]
> 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.
wdutch 22 hours ago [-]
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.
ViscountPenguin 22 hours ago [-]
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.
drivebyhooting 1 days ago [-]
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.
hangsi 1 days ago [-]
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).
p1necone 1 days ago [-]
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.
marcus_holmes 21 hours ago [-]
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?
> LLMs have been much more helpful for learning about mathematics topics than Wikipedia for a while now.
I can't imagine anyone but someone extremely gifted at first parse understanding learning mathematics from wikipedia. No effort is made to make it understandable for the average reader.
thedreammachine 22 hours ago [-]
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 also curious about training models with that singular goal. If anyone is exploring similar ideas, I'd love to chat.
drivebyhooting 22 hours ago [-]
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
thedreammachine 22 hours ago [-]
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.
mycall 22 hours ago [-]
How do you handle the 'people often learn through repetition' problem?
thedreammachine 22 hours ago [-]
[dead]
itishappy 1 days ago [-]
> If the aim of mathematics is to promote greater human understanding...
Is this the aim of mathematics?
drivebyhooting 1 days ago [-]
This is certainly what many mathematicians have used as justification for why humans should continue studying math.
kzz102 1 days ago [-]
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.
antonvs 24 hours ago [-]
> 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.
mycall 22 hours ago [-]
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.
gottheUIblues 23 hours ago [-]
Did any mathematics done by G H Hardy turn out to be quite useful in the end?
Ironically of course the answer is yes.
antonvs 18 hours ago [-]
It's not really ironic. The fact that some mathematics is useful is not an argument or evidence that the goal of mathematics is utility.
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.
feanaro 24 hours ago [-]
Even if it were not, it is a wise aim, unlike ceding understanding to a robot.
caaqil 23 hours ago [-]
> 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.
kragen 10 hours ago [-]
Are you claiming that Terry Tao in particular has expressed a contempt for teaching and pedagogy in the past? I'm not that familiar with the guy, but he always seemed to me to be the opposite — one of the more accessible Great Mathematicians at a personal level. Or are you projecting some past trauma of your own onto him?
caaqil 6 hours ago [-]
> Are you claiming that Terry Tao...
> are you projecting some past trauma
That you seem to have difficulty parsing the comment you're replying to, to the point of assuming it's about an individual rather than the community, is in itself a diagnosis that may benefit from professional help. The amateurish psychoanalysis hobby can probably wait while you get that sorted out.
wapiou 4 hours ago [-]
This one scares me
12asf1k 1 days ago [-]
[flagged]
warkdarrior 1 days ago [-]
> [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.
breezybottom 1 days ago [-]
Historically life was a lot worse.
charcircuit 1 days ago [-]
>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.
askjdfksdbfhk 1 days ago [-]
>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.
calf 1 days ago [-]
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.
pegasus 14 hours ago [-]
If you're asking why should we value something simply because humans do, the answer is simple: because we are human. It should be obvious, but it tends to get forgotten, that the ultimate goal cannot be anything other than actual human (and generally life) flourishing. Even the search for truth has to bend to this goal.
calf 5 hours ago [-]
I'm not asking why. I am pointing out that most answers here are not applying the very critical habits required of mathematics itself. The explanations and justifications are not good enough.
Revanche1367 19 hours ago [-]
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.
jltsiren 23 hours ago [-]
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.
calf 22 hours ago [-]
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.
pegasus 14 hours ago [-]
What you're saying, if I read you correctly (see note at the bottom) it that you find it unacceptable that something can be valuable simply because we find it worthwhile, without having a reason for why it is so. I don't see it like that. The capacity to reason didn't come along with a guarantee that all ignorance will evaporate instantly under the action of the scientific method. We can't just go by reason, because in many areas of our lives, reason alone doesn't go far.
PS: @calf, I've re-read your message above a few times and I must agree with others elsewhere in this thread that incoherence is afoot. Please review your own comments before sending, from the point of view of a reader who doesn't yet know what you want to say.
jltsiren 21 hours ago [-]
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.
askjdfksdbfhk 24 hours ago [-]
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?
calf 22 hours ago [-]
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.
askjdfksdbfhk 16 hours ago [-]
I have no idea what you're trying to say. Once again, if you see value in it then feel free to explain why.
The only reason most pure mathematics research exists right now is because it is interesting to the mathematicians who conduct it. I think a black box is not interesting to mathematicians and therefore has little worth. That's the argument.
mathisfun123 11 hours ago [-]
You're wasting your time - people here aren't smart/honest enough to engage with your reasoning. As someone who did math professionally for a long time, I agree with you. I think it has as much value as chess (a game we made up which we play for fun).
askjdfksdbfhk 21 minutes ago [-]
I don't really see much "reasoning" that they are presenting. Their contributions to this thread have been closer to sealioning than any kind of positive argument or thesis. What do you see in their comments that the rest of us are too stupid and dishonest to engage with, exactly?
>As someone who did math professionally for a long time, I agree with you. I think it has as much value as chess (a game we made up which we play for fun).
I mean, I don't see how this is much different from what I argued, no? Nobody really cares about computer chess all that much at this point except as a benchmark of technological achievement, and except to the extent that it helps human players better understand the game and improve their own play. We still play chess, even though computers can do it better than we can, because we find it interesting.
Revanche1367 6 hours ago [-]
A lot of people here are smart enough, they just don’t agree with the premise but maybe don’t know how to express that. Being purely for the sake of improving human understanding is more akin to philosophy than chess I’d say, and that is beneficial on its own if truly sought for that purpose.
mathisfun123 5 hours ago [-]
> A lot of people here are smart enough
they're really not because clearly their sole method of engaging with this discourse is projection.
> Being purely for the sake of improving human understanding
no matter what anyone tells you, there is absolutely no working mathematician that wakes up every day and goes to work based off that desire. it's not a priesthood, it's a job.
cindyllm 11 hours ago [-]
[dead]
cubefox 20 hours ago [-]
> 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?
charcircuit 20 hours ago [-]
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.
Revanche1367 6 hours ago [-]
The specific proof may be in pure math but Navier-Stokes problems did originate in applied math. A lot of what we consider pure math has it’s origins in something applied. As one of my math professors implied, a lot of mathematicians liked to pretend they came up with theorems from scratch in their final published form, but in practice it was often from seeing examples, often practical ones in applied math, then making conjectures that eventually led to more generalized theorems.
charcircuit 3 hours ago [-]
My point was that OpenAI did not solve the problem for a practical purpose. There is no utility to having a proof for a liquid that can't exist in reality. It was solved purely to push the frontier of what is known in mathematics.
socializer 1 days ago [-]
> 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?
charcircuit 1 days ago [-]
Important to the field of mathematics.
socializer 1 days ago [-]
"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.
sobellian 14 hours ago [-]
There are plenty of very difficult math problems with practical application. Just because they don't interest some subset of academic mathematicians does not mean they don't exist. And you don't have to literally invent a field of mathematics to do valuable work applying it (and applying it may be difficult).
charcircuit 23 hours ago [-]
>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.
lioeters 19 hours ago [-]
> exists independent from the physical realm
Doubt.
cubefox 20 hours ago [-]
If humans didn't exist, would mathematics cease to have a goal? Yes.
jibalt 1 days ago [-]
> 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.
xanderlewis 1 days ago [-]
> 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)?
goatlover 1 days ago [-]
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?
xanderlewis 1 days ago [-]
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?
oliculipolicula 6 hours ago [-]
Brace for impact.. OpenAI are going to dump their load
Looks like they are betting the downer from AGMAI is not going to hurt their cred where it matters (investors, and whales-- a mix of b-tier profs, postdocs, uni admins, and wealthy crackpots)
My own is there won't be prompts, traces, whatever, like AGMAI asked for. Same old style. Navier-Stokes "worked". People outside unglamorous analysis swallowed it.
One hope is that everyone will know someone whose years of work went for nought. By hearsay, the pipeline of whales will be broken (only hitting openAI revenues in a couple of years postIPO, however)
Your move, Anthropic
quaverquaver 1 days ago [-]
...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?
thereitgoes456 1 days ago [-]
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.
atleastoptimal 1 days ago [-]
>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.
derangedHorse 21 hours ago [-]
> 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?
greyw 1 days ago [-]
That will also happen with regulation. It's just gonna be slightly slower process
zamadatix 1 days ago [-]
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.
georgemcbay 1 days ago [-]
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.
antonvs 24 hours ago [-]
> 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.
georgemcbay 23 hours ago [-]
> 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...
conartist6 1 days ago [-]
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
dist-epoch 24 hours ago [-]
> 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"
conartist6 22 hours ago [-]
...and humanity is still here. It seems pretty resiliant.
Rendered at 22:32:27 GMT+0000 (Coordinated Universal Time) with Vercel.
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
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.
Is that true? I was under the impression they used lean as they went.
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.
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.
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.
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
I can't imagine anyone but someone extremely gifted at first parse understanding learning mathematics from wikipedia. No effort is made to make it understandable for the average reader.
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.
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.
Is this the aim of mathematics?
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.
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.
> are you projecting some past trauma
That you seem to have difficulty parsing the comment you're replying to, to the point of assuming it's about an individual rather than the community, is in itself a diagnosis that may benefit from professional help. The amateurish psychoanalysis hobby can probably wait while you get that sorted out.
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.
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.
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.
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.
PS: @calf, I've re-read your message above a few times and I must agree with others elsewhere in this thread that incoherence is afoot. Please review your own comments before sending, from the point of view of a reader who doesn't yet know what you want 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.
If you disagree (as the GP does, apparently), I ask you--what value do you see in it?
The only reason most pure mathematics research exists right now is because it is interesting to the mathematicians who conduct it. I think a black box is not interesting to mathematicians and therefore has little worth. That's the argument.
>As someone who did math professionally for a long time, I agree with you. I think it has as much value as chess (a game we made up which we play for fun).
I mean, I don't see how this is much different from what I argued, no? Nobody really cares about computer chess all that much at this point except as a benchmark of technological achievement, and except to the extent that it helps human players better understand the game and improve their own play. We still play chess, even though computers can do it better than we can, because we find it interesting.
they're really not because clearly their sole method of engaging with this discourse is projection.
> Being purely for the sake of improving human understanding
no matter what anyone tells you, there is absolutely no working mathematician that wakes up every day and goes to work based off that desire. it's not a priesthood, it's a job.
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?
>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?
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.
Doubt.
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?
Looks like they are betting the downer from AGMAI is not going to hurt their cred where it matters (investors, and whales-- a mix of b-tier profs, postdocs, uni admins, and wealthy crackpots)
My own is there won't be prompts, traces, whatever, like AGMAI asked for. Same old style. Navier-Stokes "worked". People outside unglamorous analysis swallowed it.
One hope is that everyone will know someone whose years of work went for nought. By hearsay, the pipeline of whales will be broken (only hitting openAI revenues in a couple of years postIPO, however)
Your move, Anthropic
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'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.
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.
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...
This reminds me of the early days of Covid: "it's only 10 cases, worry about the flu"