Comment by h_mirin | Hacker News Reader

Comment by h_mirin | Hacker News Reader

Parent Full thread

This is really an argument about test-time scaling, even though the post never uses the term.

These days "test-time scaling" mostly means letting the model talk to itself for longer, but the first genuinely surprising results came from plain sampling. Google's AlphaCode generated millions of candidate programs and filtered them down to a handful of submissions, which beat the average human programmer in 2022, before ChatGPT even showed up.

Sampling is what AI is good at. Making examples and doing LeetCode are similar in that verification is clear and cheap. Compared to that, "proof" is still a vague concept, except where Lean works. See the fuss over the ABC conjecture. So humans are still needed.

The interesting question to me is what happens after enough learning from "sampling." Isn't AlphaGo's move 37 an AI's nose? If that happens in mathematics, we may end up with results that are correct, machine checkable, and not explainable in any way we find satisfying.

> Google's AlphaCode generated millions of candidate programs

The trick is avoiding the infinite monkey problem. If your problem is amenable to RL, then you probably don't even need an LLM, Monte Carlo Tree Search gets you there with less expensive hardware.

> Sampling is what AI is good at.

You might think so, but I tried asking ChatGPT to solve one of the puzzles from https://en.wikipedia.org/wiki/Countdown_(game_show) (which a Python script can brute-force on my 12-year-old hardware in half a second) and it made an elementary arithmetic error that's decidedly not human-like.

LLMs are terrible at anything systematic. They're incredibly good at anything heuristic, so it makes sense that they can explore wide mathematical spaces fast and converge towards interesting regions.

But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size. You need to combine them with a proper logical problem solver to get the best parts of both.

> But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size.

It's interesting how people will comment on LLM capabilities despite clearly not having engaged with frontier models in any meaningful way in a long time

Having models write Lean proofs of mathematical claims is standard operating procedure for any LLM math discovery!

Yeah but the LLM can only handle proofs that hold inside its context window. Proofs for novel theories requiring thousands of pages with dozen millions of steps will need support from external tools to organize the full structure of the formal document; it cannot be done by the LLM inference process alone, which was my point. It would be like asking a mathematician to proof theorems without pen and paper; external tooling is a must, the statistical essential nature of generating content from weights is 1) error prone and 2) not suitable for chains of systematic reasoning that are longer than the attention span.

The proofs will be only as good as the framework for linking successive instances of reasoning.

Not sure how true this restrictions is once you have the agents hammering on at a big code base of formalised proofs.

Proofs stretching thousands of pages are split into lemmas, grouped into sub theories.

What I haven’t seen agents do yet is to develop new ideas for entire such theories. I have usually seen them bite into some existing idea and grinding out related results. But I am less sure than ever that they won’t!

The thread title is "What sort of maths are LLMs good at?"

The codebase you describe would be an external tool in GP's conception.

If I walked outside, I would also be an external tool. So, I don't.

Every LLM harness released in the last year has handled this gracefully via delegation, structured memory systems, etc.

"ChatGPT" could mean anything from Instant to Pro. What was the prompt, and which model(s) did you try?

Almost surely the free model on the web ui. So a dumb model, no harness, and probably a bad prompt.

My point was that the kind of error it made was nothing like the kind of error a contestant would make.

The differences between 'instant' chat models and frontier-grade models are enough to render any such test a waste of electricity.

for somebody who's out of the loop: what's the fuss over the ABC conjecture?

This is a reference to Inter-Universal Teichmüller Theory. Its Wikipedia article gives a good overview (https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll...). In maths lasting disagreements over a published "proof" are rare, but IUTT is an example of it. What the article misses: There is a more recent, ongoing effort to formalize the published proof in Lean under the name of "LANA" (e.g. see https://zen.ac.jp/news/zmcpostevent0717e and https://github.com/katobungen/LANA_report_202607/blob/pdf/LA... for a recent update). I guess most mathematicians agree that a successful compile of the proof in Lean would confirm its validity. My personal impression is that the process got stuck at the very point Peter Scholze and Jakob Stix pointed out 8 years ago. Officially LANA has still not reached a conclusion.

> Peter Scholze and Jakob Stix pointed out 8 years ago

Interesting read!

https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...

TDLR for the other two comments: a Japanese mathematician is claiming to have a proof for it, but it is based on an entirely new very complex field of maths which he invented. Getting into it takes years, so other mathematicians are hesitant to invest that much time only to find out that the proof is broken and the field isn't otherwise useful.

It doesn't help that the author is rather withdrawn and not willing to spend any effort in making it more approachable.

Some tried, and said they found gaps in the proof, to which the author responded, but they were not convinced.

And that's essentially the situation since 2018.

https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll...

Wikipedia is maybe the narrow end of a wedge into this topic but the controversy revolves around a very large and very complex paper that few people are equipped to understand and some of those who are able believe the proof is false.

> we may end up with results that are correct, machine checkable, and not explainable in any way we find satisfying

sounds like quantum mechanics

Reply on news.ycombinator.com