Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A misalignment of AI in mathematics

mathandai.org

Post reply on HN
Print view View original

611–620 of 646 posts

Re: A misalignment of AI in mathematics

#611

Post by Xirdus »

stabbles wrote: post #519
psvv wrote: post #453

Earlier quoted context omitted.

I think the parent comment meant professional, high-level chess. The kind people get played to play, not just do for a hobby. That's absolutely on life support. I'm not sure what the equivalent would look like in the math field, but it probably involves a lot of mathematicians losing their jobs and the quality of human-produced math decreasing overall. The quality of the math in general would be fine, since in this s…

Mathematics is more than establishing arbitrary facts (although some look like curiosities), it's also defining what interesting research directions are and establishing common language/notation. I think that will stay relevant?

In theory you can automate finding interesting research directions by identifying conjectures with many dependencies. And notation has never been mathematicians' forte, with them trying to cram the entirety of universe into single letters.

Re: A misalignment of AI in mathematics

#612

Post by ndriscoll »

SpicyLemonZest wrote: post #412
yieldcrv wrote: post #373

Earlier quoted context omitted.

Different person here, I read the article and they are all wrong. Hope that helps. Okay, to elaborate, substantively, their point is that the people using these AI models are not doing it for the love of the game, but for marketing. And instead of them - and nobody - spending millions of dollars to solve the problem, successfully, they want every problem of their academic industry to persist because even though they…

Their claim is only indirectly related to the motivations of the people using their models. What they're saying is that doing math in this way does not produce the same value as traditional mathematical research, and the people using these AI models aren't concerned about that because their marketing objectives don't depend on whether their results produce mathematical value. If people doing valuable work are made ir…

But it does produce value. We now have an explicit solution and even a proof. Humans can then work on clarifying why it's true. Unsurprisingly, not all that different from software, where models can generate working code just fine. The details will all be there and all correct, but the architecture is currently not ideal, so a human guiding it can greatly improve the proofs.

I actually found this to be the case with some basic linear algebra notes I was recently doing in Lean (without using mathlib). The model could generate working proofs, but they obscure the basic ideas (actually I wonder somewhat if this is because the Lean code that's out there to train on doesn't make a huge effort to read like textbook proofs, which was my motivation in the first place). I give it a skeleton of a couple lines of `calc`, letting it fill in the reasoning for each line, and it does much better. Then ask it about making some macros to simplify "trivial" or "obvious" things, and it does even better. etc.

I suspect there's a good workflow where a big SOTA model makes an impenetrable proof (or code) and then a human works with a FIM model to simplify it (with the larger gnarly proof right there in context for FIM), but unfortunately everyone seems to only care about agents right now.

Re: A misalignment of AI in mathematics

#613

Post by genxy »

DoctorOetker wrote: post #534
genxy wrote: post #439

Earlier quoted context omitted.

Math department administrators fire Terence Tao. Based on current reward models, the frontier AI labs will burn down mathematics as an impressive display of capabilities and in doing so, will make it impossible for people that get paid to do mathematics to stay employed. If your job is literally to publish papers, and OpenAI and Anthropic decide that making an infinite-paper-printing machine is the best thing to show…

I wouldn't expect them to destroy that industry, imagine global squadrons of academics and mathematicians focusing their attention on LLM's, training algorithms, scaling laws, ... they're gonna try and beat the incumbent frontier AI labs, eye for an eye, tooth for a tooth

The apocalypse being triggered by frontier labs picking a fight with mathematicians was unexpected.

Re: A misalignment of AI in mathematics

#614

Post by nilkn »

suddenlybananas wrote: post #321
CuriouslyC wrote: post #311

Earlier quoted context omitted.

Given the witch hunts around AI creative output, nobody who has put in work to avoid the stigma is going to out themselves.

Why would they have had to put work in?

The work is either: (1) the act of concealment: generating an AI book that cannot be detected as AI generated; or (2) actually just writing the book yourself.

Re: A misalignment of AI in mathematics

#615

Post by sweezyjeezy »

fph wrote: post #539
tmhn2 wrote: post #200

As a mathematician maybe I am a little more optimistic than this declaration. I am thinking of Mochizuki's abc conjecture: He worked in relative isolation, and dumped a huge incomprehensible proof on the community (to oversimplify a bit). That's not totally unlike what might happen if AI generates a huge, incomprehensible proof of let's say RH. Well, what is the result? In the Mochizuki case, it was a lot of skeptici…

> Maybe mathematics just becomes a little more like other fields--relying on labs with lots of money for compute, digging through a corpus of AI-generated proofs, etc. I think a better comparison is: mathematics just becomes like mining bitcoins.

I think you might have to explain that comparison a bit more to be honest. How are math proofs like bitcoins? A bitcoin has a pre-defined value, a math conjecture / proof is a bit more complicated.

Re: A misalignment of AI in mathematics

#616

Post by curt15 »

jrflo wrote: post #276
9question1 wrote: post #221

Earlier quoted context omitted.

That's precisely the problem though. You cannot still read and understand an AI written proof at the current skill level of the AI being applied, because they're orders of magnitude longer than human written proofs even when they don't need to be, and spend most of that length on the parts that aren't important. This has been really thoroughly documented by expert mathematicians who are engaging with AI in public lik…

That doesn't seem to be true. The OpenAI NS paper was 166 pages. Wiles-Taylor proof of Fermat's last theorem is 129 pages. The length is not unprecedented for a difficult unsolved problem. To be honest, I feel like the difficulty of reading AI proofs is due to the fact that we are on the verge of being beyond human comprehension. This is a demonstrable fact as no human has figured this out despite the problem being o…

> This is a demonstrable fact as no human has figured this out despite the problem being open for almost 100 years.

That's not true. Alpoge and Buckmaster's related LLM-assisted blowup result (https://news.ycombinator.com/item?id=49605915) utilized a strategy developed recently by Cordoba and Martinez-Zoroa.

Re: A misalignment of AI in mathematics

#617

Post by ls612 »

Creamsicle47 wrote: post #556
keeda wrote: post #427

I understand this stance and where they are coming from, but I can't help but think this sounds very analogous to engineers' arguments against AI-assisted and vibe-coding, especially with regard to cognitive debt. Yet the software industry is plowing ahead, reportedly pushing mountains of unreviewed code to Prod, and the world hasn't ended. Of course, nobody's really comfortable with it, so this is also a forcing fun…

> Yet the software industry is plowing ahead, reportedly pushing mountains of unreviewed code to Prod, and the world hasn't ended. Yes, this has gone so well

It really has. All of the places facing an unusually high outage rate are places that have seen huge growth in their service usage (Anthropic, GitHub, etc) which is to be expected. The rest of the world has been happily chugging along with coding agents for almost a year now and things seem to still be working just fine.

Re: A misalignment of AI in mathematics

#618

Post by jeremyjh »

flatline wrote: post #521
robotpepi wrote: post #447

Earlier quoted context omitted.

It makes no sense to compare mathematics with chess. Chess is a sport. No one is interested in watching two machines compete. Chess doesn't have a practical impact. Etc. What you seem to suggest is that AI will be able to completely (or at least in a great part) replace mathematicians. It could be the case in the future, but no one knows right now, and more importantly: tech companies don't even think about it! they…

Does mathematics still have a practical impact without humans in the loop? I don't think there's one single answer to that question, but I think it's worth considering exactly what that impact may be. Tech companies are as much the topic of this post as AI, I think that's the immediacy.

To a significant extent, the pursuit of mathematics research is a pursuit of human understanding of mathematics, without knowing where it might lead, or whether it might lead anywhere at all. I don't see how the motivation for that goes away on its own, but the institution supporting it is certainly threatened by the potential loss of grant money and graduate student applications.

Re: A misalignment of AI in mathematics

#619

Post by krupan »

I don't know, people. We still really don't know how OpenAI or others are producing these results. It's all very hand wavy and trust-me-bro. How much money/time/compute have they really thrown at these problems? How much human involvement was there? What LLM did they even use? How much regular software was involved? They have given answers to some of those questions but no proof that that's actually what they did. I don't know if it's worth giving them this much credit (which is what we are doing by writing these essays and spending so much time debating). Anthropic wrote a C compiler that turned out to not really be a ready made replacement for GCC. Did they ever do any more work on it? Has anyone else produced a C compiler? It seems like that and these proofs are just demoware that are not (yet? Who knows?) production ready to turn the world upside down. Impressive one-off demos, yes, but companies have been pulling those off for centuries without ever going anywhere afterwards.

Re: A misalignment of AI in mathematics

#620

Post by bwfan123 »

magicalist wrote: post #361
causalmodels wrote: post #269

Earlier quoted context omitted.

What do we do about the problems that don't require many millions of dollars in resources? Last weekend I spun up a small agent swarm and pointed it at a field of math I have some affinity towards. Within four hours I had settled three conjectures, one of which is rather famous (for the field, not in general). It cost me about four hundred dollars. I am at a loss about what to do with these results. On one hand I fee…

I mean, let's say you spun up a swarm of agents to rewrite a large component of a well used open source library to be memory safe. You could dump it in a big PR and walk away (we all know how that would go), or you could try engaging, see if they're interested, write something up and see where it goes. The biggest problem is, IMO, drivebys uninterested in actual results, just getting a check mark, and the equivalent…

> and the equivalent of dropping a 200k line PR on people

With the equivalence of code as proofs, what you said is literally true.

I see it as Brandolini's principle on steroids and can understand why the community is pissed. So now, lean proofs can be churned out at scale, and the community is left to decipher all of that slop into human understanding. There are bad actors with misaligned incentives coming in with drive-by proofs upending what the community holds dear which is to practice and propagate the art.

To re-align incentives the following should happen. AI slop lean proofs are dumped unceremoniously into a lean dumpster, and prizes are only awarded to papers that explain results that could digested into human understanding - via the already followed human review process. Prizes are not given to lean proofs since anyone with sufficient compute can churn them out.

Post reply on HN