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

First Proof

arxiv.org

Post reply on HN
Print view View original

101–110 of 126 posts

Re: First Proof

#101

Post by gaogao »

ozgung wrote: post #100

This is exciting as a reality check of our expectations from the current level of AI. I expect AIs to solve at least 2-3 of them in a week. I expect one “easy” problem that multiple models solve. And I expect at least one solution to be “interesting” and different than the human solutions. I also expect human researchers to solve more than AIs in a week (globally, by total) but I don’t know what happens if they publi…

Yeah, I pointed a custom thing and Claude at #6, and it's solved it in Lean besides needing to axiomize one theorem not in mathlib. Only about four of the problems have enough foundations formalized in mathlib though for this approach.

Re: First Proof

#102

Post by stevage »

pegasus wrote: post #56
nemo1618 wrote: post #33

Earlier quoted context omitted.

Centaurs are a transient phenomenon. In chess, the era of centaur supremacy lasted only about a decade before computers alone eclipsed human+computer. The same will be true in every other discipline. You can surf the wave, but sooner or later, the wave will come crashing down.

They are transient only in those rare domains that can be fully formalized/specified. Like chess. Anything that depends on the messy world of human - world interactions will require humans in the loop for translation and verification purposes.

>Anything that depends on the messy world of human - world interactions will require humans in the loop for translation and verification purposes.

I really don't see why that would necessarily be true. Any task that can be done by a human with a keyboard and a telephone is at risk of being done by an AI - and that includes the task of "translation and verification".

Re: First Proof

#104

Post by pegasus »

stevage wrote: post #102
pegasus wrote: post #56

Earlier quoted context omitted.

They are transient only in those rare domains that can be fully formalized/specified. Like chess. Anything that depends on the messy world of human - world interactions will require humans in the loop for translation and verification purposes.

>Anything that depends on the messy world of human - world interactions will require humans in the loop for translation and verification purposes. I really don't see why that would necessarily be true. Any task that can be done by a human with a keyboard and a telephone is at risk of being done by an AI - and that includes the task of "translation and verification".

Sure, but at the risk of running into completely unforeseen and potentially catastrophic misunderstandings. We humans are wired to use human language to interact with other humans, who share our human experience, which AIs can only imperfectly model.

Re: First Proof

#105

Post by pegasus »

Davidzheng wrote: post #97
pegasus wrote: post #56

Earlier quoted context omitted.

They are transient only in those rare domains that can be fully formalized/specified. Like chess. Anything that depends on the messy world of human - world interactions will require humans in the loop for translation and verification purposes.

Sure, but in pure mathematics there are a lot of well specific problems which no one can solve.

Mathematics is indeed one of those rare fields where intimate knowledge of human nature is not paramount. But even there, I don't expect LLMs to replace top-level researchers. The same evolutionary "baggage" which makes simulating and automating humans away impossible is also what enables (some of) us to have the deep insight into the most abstract regions of maths. In the end it all relies on the same skills developed through millions of years of tuning into the subtleties of 3D geometry, physics, psychology and so on.

Re: First Proof

#106

Post by seanhunter »

noosphr wrote: post #67
nemo1618 wrote: post #33

Earlier quoted context omitted.

Centaurs are a transient phenomenon. In chess, the era of centaur supremacy lasted only about a decade before computers alone eclipsed human+computer. The same will be true in every other discipline. You can surf the wave, but sooner or later, the wave will come crashing down.

Last I heard, which was last year, human + computer still beat either by themselves. You got a link about what's changed?

The last public ranking of chess centaurs was 2014, after which it is generally held to be meaningless as the ranking of a centaur is just the same as the ranking of the engine. Magnus Carlsen’s peak elo of 2884 is by far the highest any human has ever achieved. Stockfish 18 is estimated to be in excess of 4000 elo. Which is to say the difference between it and the strongest human player ever is about the same as the difference between a strong club player and a grandmaster. It’s not going to benefit meaningfully from anything a human player might bring to the partnership.

Magnus himself in 2015 said we’ve known for a long time that engines are much stronger than humans so the engine is not an opponent.

https://stockfishchess.org/blog/2026/stockfish-18/

https://www.dw.com/en/world-chess-champion-magnus-carlsen-th...

Re: First Proof

#107

Post by pas »

pegasus wrote: post #104
stevage wrote: post #102

Earlier quoted context omitted.

>Anything that depends on the messy world of human - world interactions will require humans in the loop for translation and verification purposes. I really don't see why that would necessarily be true. Any task that can be done by a human with a keyboard and a telephone is at risk of being done by an AI - and that includes the task of "translation and verification".

Sure, but at the risk of running into completely unforeseen and potentially catastrophic misunderstandings. We humans are wired to use human language to interact with other humans, who share our human experience, which AIs can only imperfectly model.

I have to say I don't feel this huge shared experience with many service industry workers. Especially over the phone. We barely speak the same language!

Re: First Proof

#108

Post by _alternator_ »

data_maan wrote: post #87
_alternator_ wrote: post #72

Earlier quoted context omitted.

I’m confused by this comment. I’m pretty sure that someone at all the bigs labs is running these questions through their models and will report back as soon as the results arrive (if not sooner, assuming they can somehow verify the answers). The fact that you find it odd that this landed on arXiv is maybe a cultural thing… mathematicians kinda reflexively throw work up there that they think should be taken seriously.…

Yes, but people at those labs may be running those problems because a Fields Medalist is in the paper, and it got hype. Not because of the problems, and not because this is new methodology. And once the labs report back, what do we know that we didn't know before? We already know, as humans, the answer to the problems, so that is not it. We already know that LLMs can solve some hard problems, and fail in easy problem…

Ah. I think the issue is that research mathematicians haven’t yet hit the point where the big models are helping them on the problems they care about.

Right now I can have Claude code write a single purpose app in a couple hours complete with a nice front end, auth, db, etc. (with a little babysitting). The models solve a lot of the annoying little issues that an experienced software developer has had to solve to get out an MVP.

These problems are representative of the types of subproblems research mathematicians have to solve to get a “research result”. They are finding that LLMs aren’t that useful for mathematical research because they can’t crush these problems along the way. And I assume they put this doc together because they want that to change :)

Re: First Proof

#109

Post by w-m »

An iterative prompt with GPT-5.2 on Copilot CLI spits out a dense two-page proof for problem 10 after less than 60 minutes of working. A review of the generated proof with Claude 4.6 on Copilot attests it mathematical correctness, identifying only minor issues, mostly in the presentation.

But as a non-mathematician I'm not following any of it. How many people are there who are willing to check the generative results? And how much effort is it for a human to check these? How quickly can you even identify math-slop?

Here's the generated proof:

https://github.com/w-m/firstproof_problem_10/blob/2acd1cea85...

Re: First Proof

#110

Post by nxobject »

Davidzheng wrote: post #96
okintheory wrote: post #94

Earlier quoted context omitted.

I think you're misunderstanding the point this paper is trying to make. They're interested in trying to distinguish whether AI is capable of solving new math problems or only capable of identifying existing solutions in the literature. Distinguishing these two is difficult, because self-contained math problems that are easy enough for LLMs to address (e.g. minor Erdos-problems) may have been solved already as subcomp…

I find it unbelievable that this question can't be settled themselves without posting this simply by asking the AI enough novel questions. I myself have little doubt that at least they can solve some novel questions (of course similarity of proofs is a spectrum so it's hard to draw the line at how original they are)

Trust, but verify, no? No one benefits from refusing to experiment and test.
Post reply on HN