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.

▲

laszlojamf 5 hours ago | parent | next [-]

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

	▲	steinwinde 5 hours ago \| parent \| next [-]
		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.
	▲	pringk02 5 hours ago \| parent \| prev \| next [-]
		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.
	▲	brazzy 2 hours ago \| parent \| prev [-]
		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.

▲

jgalt212 4 hours ago | parent | prev [-]

> 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.