Live data from Hacker News

The AI revolution in math has arrived

quantamagazine.org

51–60 of 68 posts

Re: The AI revolution in math has arrived

#51

Earlier quoted context omitted.

It was just yesterday that this top post [] was decrying the "peril of laziness lost", that LLMs inherently lack the virtue of laziness. So which one are they? [] https://news.ycombinator.com/item?id=47743628

I think laziness is not a minimum of effort. Laziness can actually be more effort towards a simpler or more practical solution, because those solutions are more pleasant in some way, and therefore more attractive to pursue.

Reminds me of Larry Wall's three virtues of a programmer: laziness, impatience and hubris.

Re: The AI revolution in math has arrived

#52
post #28

Last week I got together with my math alumni friend. We cracked some beers, we chatted with voice mode ChatGPT and toyed around with Collatz Conjecture and we sent some prompt to a coding agent to build visualizations and simulation. It was a lot of fun directing these agents while we bounced off ideas and the models could explore them. I think with the right problem and the right agentic loop it’s clear to me improv…

I think voice mode uses weaker models, just an FYI relative to the SOTA

Can get around this with a local STT model and use text input but UX is probably clunkier

Re: The AI revolution in math has arrived

#53
post #39

Mathematics seems like the ideal candidate for AIs to achieve absurd results. It's a purely abstract grammar with true auto-verifiability. Even SWE has the requirement of interacting with real physical things. In math there's no external feedback required, you're solely bounded by the rate and quality of token generation.

Grammar seems like you’re talking about LLMs specifically. Well, isn’t Sudoku just math? LLMs suck at Sudoku last I checked. When told not to code a solver, its very first deduction was wrong.

Generally when people talk about using LLMs to do mathematics research they’re not talking about the LLM alone, but the LLM + a harness for it to write and execute theorem provers such as Lean or Coq to validate their results.

Re: The AI revolution in math has arrived

#54
post #28

Last week I got together with my math alumni friend. We cracked some beers, we chatted with voice mode ChatGPT and toyed around with Collatz Conjecture and we sent some prompt to a coding agent to build visualizations and simulation. It was a lot of fun directing these agents while we bounced off ideas and the models could explore them. I think with the right problem and the right agentic loop it’s clear to me improv…

I think voice mode uses weaker models, just an FYI relative to the SOTA

The bigger problem for me is that the realtime voice modes lack tool use, so they can't look anything up or do anything. Model strength definitely also matters, but even dumb models can be helpful when they can look things up and try things out. And smart models that don't do those things kinda suck.

Re: The AI revolution in math has arrived

#55

Earlier quoted context omitted.

You just failed the Turing test.

The Turing test just failed you. I'll go one better, physics isn't reality, it's a model of reality utilizing math.

And I'll go one better, you haven't said anything here at all, you've just left a representation of what you understand to be saying.

Re: The AI revolution in math has arrived

#57

Mathematics seems like the ideal candidate for AIs to achieve absurd results. It's a purely abstract grammar with true auto-verifiability. Even SWE has the requirement of interacting with real physical things. In math there's no external feedback required, you're solely bounded by the rate and quality of token generation.

This misses the mark on at least two accounts: 1. Proofs without human understanding have less value for mathematicians 2. At least for now, interestingness depends on human judgment. It is subjective and not as verifiable.

1. The four color theorem is a useful case study, for which the original proof was validated and 400 pages long. My prediction is that the first couple waves of proofs will be hard enough that a layman couldn't produce them, but simple enough that experts can verify them. Over time the most advanced proofs will get more and more complicated until humans can no longer verify them, this process could happen over the course of a few month or could take literally hundreds of years.

2. Especially early on the overwhelming majority of the proofs are likely to be uninteresting and more novel just because actually producing them would take expert time that's better spent elsewhere. That being said, as above over time I expect the interestingness of proofs to go up until they eventually regularly produce interesting proofs. The vast majority of proofs are likely to maintain their position as of no interest to humans for the simple reason that the vast majority of proofs are of no interest to humans.

In neither case will I make any particular guesses about a timeline beyond it seems like the way things will go.

Re: The AI revolution in math has arrived

#58

Earlier quoted context omitted.

You just failed the Turing test.

Fortunately for me equivalents to Turing exist: https://en.wikipedia.org/wiki/Turing_machine_equivalents

I don't follow. Can you explain how your comment is relevant to mine? It might help if you also explain how you interpreted my comment.

Re: The AI revolution in math has arrived

#59

> As they did so, they also learned how to improve the prompts they gave AlphaEvolve. One key takeaway: The model seemed to benefit from encouragement. It worked better “when we were prompting with some positive reinforcement to the LLM,” Gómez-Serrano said. “Like saying ‘You can do this’ — this seemed to help. This is interesting. We don’t know why.” Four top logical people in the world are acknowledging this. It is…

I know why. Several people had problems with Sonnet burning through all their credits grinding on a problem it can't solve. Opus fixes this — it has a confidence threshold below which it exits the task instead of grinding. "I spent ~$100 last week testing both against multiplication. Sonnet at 37-digit × 37-digit (~10³⁷) never quits — 15+ minutes, 211KB of output, still actively decomposing numbers when I stopped it.…

From my reading, the official docs don’t support the strong claim that frontier LLMs are explicitly RL-trained to “be lazy” or conserve tokens as claimed in this thread. What they do document is adaptive / hidden reasoning compute: OpenAI says reasoning models allocate internal reasoning tokens and reasoning.effort controls how many are used (https://developers.openai.com/api/docs/guides/reasoning), and Anthropic says adaptive thinking decides whether/how much to use extended thinking based on request complexity, with effort as soft guidance and max_tokens as the hard cap (https://docs.anthropic.com/en/docs/build-with-claude/adaptiv... hinking). So prompt wording may change how the same budget is spent, but it can’t exceed the hard token cap.

Also, the “encouragement helps” anecdote seems real in the AlphaEvolve workflow, but I can't see that forpublic models. Gómez-Serrano says this in Quanta (https://www.quantamagazine.org/the-ai-revolution-in-math-has... rived-20260413/), and the released AlphaEvolve notebooks really do contain prompts like “Good luck, I believe in you...” (https://github.com/google-deepmind/alphaevolve_repository_of... oblems, e.g. https://github.com/google-deepmind/alphaevolve_repository_of... blems/blob/main/experiments/finite_field_kakeya_problem/finite_f ield_kakeya.ipynb). But those prompts also bundled strong structural hints (“find a general solution”, “better constructions are possible”), so from my reading the evidence is: prompt phrasing matters, especially in an internal search stack, but not “pep talks are a universal reasoning hack.”

Re: The AI revolution in math has arrived

#60
post #39

Earlier quoted context omitted.

Grammar seems like you’re talking about LLMs specifically. Well, isn’t Sudoku just math? LLMs suck at Sudoku last I checked. When told not to code a solver, its very first deduction was wrong.

Generally when people talk about using LLMs to do mathematics research they’re not talking about the LLM alone, but the LLM + a harness for it to write and execute theorem provers such as Lean or Coq to validate their results.

I guess I just don’t have the experience or optimism that a harness around an LLM, which can’t make the first, bare deduction on its own, is a good use of compute.

I got out of RLHF, including games and puzzles, before agents took off and maybe I have outdated info. But we estimated RLHF’ing a single hard full sized sudoku was ~25 hours worth of work.

Post reply on HN