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

“Erdos problem #728 was solved more or less autonomously by AI”

mathstodon.xyz

Post reply on HN
Print view View original

301–310 of 385 posts

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#301

Post by j_maffe »

tomjen3 wrote: post #279
maxwells-daemon wrote: post #166

Earlier quoted context omitted.

For this reason, when we announce results on e.g. the IMO, we formalize the statements by hand and inspect the proofs carefully to ensure they capture the full spirit of the problem. However, there are some good heuristics. If you expect a problem to be hard and the proof is very short, you've probably missed something!

Aren't the best proofs very short?

"Best" is subjective. Proofs can get very long especially for the harder ones mathematicians are tackling these days.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#302

Post by phyzome »

codeflo wrote: post #262
ccppurcell wrote: post #222

Earlier quoted context omitted.

Are you an expert? Not gatekeeping here but I have no intuition for what is easy or hard to formalise. A lot of very simply stated graph theoretical results are apparently extremely hard to formalise.

> apparently When someone takes the time to explain undergrad-level concepts in a comment, responding with "are you an expert?" is a level of skepticism that's bordering on hostile. The person you're responding to is correct, it's rare that the theorem statement itself is particularly hard to formalize. Whatever you read likely refers to the difficulty of formalizing a proof.

I think it was a fine question to ask in the context of a discussion of epistemology.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#303

Post by ogogmad »

jacquesm wrote: post #204
MyFirstSass wrote: post #87

Earlier quoted context omitted.

I'm not sure i understand the wild hype here in this thread then. Seems exactly like the tests at my company where even frontier models are revealed to be very expensive rubber ducks, but completely fails with non experts or anything novel or math heavy. Ie. they mirror the intellect of the user but give you big dopamine hits that'll lead you astray.

This accurately mirrors my experience. It never - so far - has happened that the AI brought any novel insight at the level that I would see as an original idea. Presumably the case of TFA is different but the normal interaction is that that the solution to whatever you are trying to solve is a millimeter away from your understanding and the AI won't bridge that gap until you do it yourself and then it will usually pr…

The problem is unclear. I think you have a labelled graph G=(V, E) with labels c:V->R, such that each node in V consists of a triple (L, R, S) where L is a sequence of weights are on the left, R is a sequence of weights that are on the right, and S is a set of weight that have been taken off. Define c(L, R, S) to be the centre of mass. Introduce an undirected edge e={(L, R, S), (L', R', S')} between (L, R, S) and (L', R', S') either if (i) (L', R', S') results from taking the first weight off L and adding it to S, or (ii) (L', R', S') results from taking the first weight off R and adding it to S, or (iii) (L', R', S') results from taking a weight from W and adding it to L, or (iv) (L', R', S') results from taking a weight from W and adding it to R.

There is a starting node (L_0, R_0, {}) and an ending node ({}, {}, W) , with the latter having L=R={}.

I think you're trying to find the path (L_n, R_n, S_n) from the starting node to the ending node that minimises the maximum absolute value of c(L_n, R_n, S_n).

I won't post a solution, as requested.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#304

Post by jacquesm »

ogogmad wrote: post #303
jacquesm wrote: post #204

Earlier quoted context omitted.

This accurately mirrors my experience. It never - so far - has happened that the AI brought any novel insight at the level that I would see as an original idea. Presumably the case of TFA is different but the normal interaction is that that the solution to whatever you are trying to solve is a millimeter away from your understanding and the AI won't bridge that gap until you do it yourself and then it will usually pr…

The problem is unclear. I think you have a labelled graph G=(V, E) with labels c:V->R, such that each node in V consists of a triple (L, R, S) where L is a sequence of weights are on the left, R is a sequence of weights that are on the right, and S is a set of weight that have been taken off. Define c(L, R, S) to be the centre of mass. Introduce an undirected edge e={(L, R, S), (L', R', S')} between (L, R, S) and (L'…

You are overthinking it.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#305

Post by encyclopedism »

MyFirstSass wrote: post #87
D-Machine wrote: post #76

Earlier quoted context omitted.

You're understanding correctly, this is back and forth between Aristotle and ChatGPT and a (very smart) user.

I'm not sure i understand the wild hype here in this thread then. Seems exactly like the tests at my company where even frontier models are revealed to be very expensive rubber ducks, but completely fails with non experts or anything novel or math heavy. Ie. they mirror the intellect of the user but give you big dopamine hits that'll lead you astray.

Lots of users seem to think LLM's think and reason so this sounds wonderful. A mechanical process isn't thinking, certainly it does NOT mirror human thinking. The processes being altogether different.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#306

Post by tetha »

ccppurcell wrote: post #222
ndriscoll wrote: post #179

Earlier quoted context omitted.

The problem statement is apparently > Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn? Which seems like it's the type of thing you give as a homework problem to state formally in an intro class.

Are you an expert? Not gatekeeping here but I have no intuition for what is easy or hard to formalise. A lot of very simply stated graph theoretical results are apparently extremely hard to formalise.

As the sibling comment says, in my experience, the difficulty of formalizing the problem varies greatly between different areas. Probability theory is another notorious field in which modelling a problem correctly can be very subtle and difficult.

On the other hand, many problems in number theory and discrete structures tend to be rather simple to formalize. If you want to take your own look at that, I'd recommend to check out the lean games[1]. I'd say after the natural numbers game, you most likely know enough lean to write that problem down in lean with the "sufficiently small" being the trickiest part.

1: https://adam.math.hhu.de/

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#307

Post by naasking »

MyFirstSass wrote: post #64

Based on Tao’s description of how the proof came about - a human is taking results backwards and forwards between two separate AI tools and using an AI tool to fill in gaps the human found? I don’t think it can really be said to have occurred autonomously then? Looks more like a 50/50 partnership with a super expert human one the one side which makes this way more vague in my opinion - and in line with my own AI test…

> EDIT: I can see the title has been fixed now from solved to "more or less solved" which is still think is a big stretch.

"solved more or less autonomously by AI" were Tao's exact words, so I think we can trust his judgment about how much work he or the AI did, and how this indicates a meaningful increase in capabilities.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#308

Post by threatofrain »

mjevans wrote: post #173
sibrahim wrote: post #158

Earlier quoted context omitted.

That's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Given a formal statement of what you want, Lean can validate that the steps in a (tedious) machine-readable purported proof are valid and imply the result from accepted axioms. This is not AI, but a tiny, well reviewed kernel that only accepts correct formal logic arguments. So, if you have a formal statement that you'v…

I think the question is, how can humans have verification that the problem statement was correctly encoded into that Lean specification?

It’s far easier for Lean because the human has to read very little compared to generating whole programs.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#309

Post by kelipso »

codeflo wrote: post #262
ccppurcell wrote: post #222

Earlier quoted context omitted.

Are you an expert? Not gatekeeping here but I have no intuition for what is easy or hard to formalise. A lot of very simply stated graph theoretical results are apparently extremely hard to formalise.

> apparently When someone takes the time to explain undergrad-level concepts in a comment, responding with "are you an expert?" is a level of skepticism that's bordering on hostile. The person you're responding to is correct, it's rare that the theorem statement itself is particularly hard to formalize. Whatever you read likely refers to the difficulty of formalizing a proof.

Lol it’s weird seeing high school redditors saying gatekeeping and are you an expert in the same thread as university professors, all talking about the same topic. But I guess that’s HN for you.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#310

Post by semi-extrinsic »

charcircuit wrote: post #192
semi-extrinsic wrote: post #69

Earlier quoted context omitted.

This idea is just ridiculous to anyone who's worked in academia. The theory is nice, but academic publishing is currently in the late stages of a huge death spiral. In any given scientific niche, there is a huge amount of tribal knowledge that never gets written down anywhere, just passed on from one grad student to the rest of the group, and from there spreads by percolation in the tiny niche. And papers are never h…

The same could be said about programmers, but we have adapted and started writing it all down so that AI cab use it.

No no, in comparison to academia, programmers have been extremely diligent at documenting exactly how stuff works and providing fairly reproducible artifacts since the 1960s.

Imagine trying to teach an AI how to code based on only slide decks from consultants. No access todocumentation, no stack overflow, no open source code used in the training data; just sales pitches and success stories. That's close to how absurd this idea is.

Post reply on HN