Merged Artificial Intelligence

[W.D.Clinger]

any math nerds take a look at that chatgpt ai math problem document dump?

Are you talking about Erdős Problem #1196? (ETA: Proof here.)

Or are you talking about using ChatGPT for homework problems?

Or something altogether different? (ETA: Such as the Navier-Stokes Millennium Prize Problem, which has been proof-checked by the Lean proof assistant; the AI solution to Erdős Problem #1196 has also been checked by Lean. Lean, by the way, uses a hygienic macro system, so I can tell myself I made my own extremely tiny contribution to the AI solutions of those two problems.)

Yes there are use cases for LLMs, but the cases where they approach even moderate human capabilities are so few and far between that they'll only ever be hobbyist curios.

In my opinion, that proof of Erdős Problem #1196 approaches moderate human capabilities. To put it even more strongly: I daresay the number of humans who could have come up with that proof on their own is exceeded by the number of humans who could not have done so.

(The existence of a bound was proved in 1935, and a particular bound was conjectured in 1968. That conjecture was not proved by a human until 2022. Prompted by Liam Price, GPT-5.4 Pro found another proof in April 2026.)

 

[dirtywick]

Are you talking about Erdős Problem #1196? (ETA: Proof here.)

Or are you talking about using ChatGPT for homework problems?

Or something altogether different? (ETA: Such as the Navier-Stokes Millennium Prize Problem, which has been proof-checked by the Lean proof assistant; the AI solution to Erdős Problem #1196 has also been checked by Lean. Lean, by the way, uses a hygienic macro system, so I can tell myself I made my own extremely tiny contribution to the AI solutions of those two problems.)

In my opinion, that proof of Erdős Problem #1196 approaches moderate human capabilities. To put it even more strongly: I daresay the number of humans who could have come up with that proof on their own is exceeded by the number of humans who could not have done so.

(The existence of a bound was proved in 1935, and a particular bound was conjectured in 1968. That conjecture was not proved by a human until 2022. Prompted by Liam Price, GPT-5.4 Pro found another proof in April 2026.)

OpenAI releases 372 math result groups on GitHub

The 722 papers span number theory, algebraic geometry, and other fields, and include advances related to 3 remaining Millennium Prize Problems

tech.yahoo.com

i was asking about this story.

 

[The Great Zaganza]

is that the one they mostly stole from researchers?

 

[Andy_Ross]

You are all the ENEMY!

Donald J. Trump
@realDonald Trump

The White House considers anyone that uses the term, "Artificial Intelligence," as opposed to the highly accepted new and more accurate term, "Super Intelligence," THE ENEMY!

President DONALD J. TRUMP

 

[carlosy]

Can we be certain, that some A.I. isn't already in the White House IT, blackmailing Trump et al.?

Can we?

 

[Helen]

"Highly accepted". I'm sorry to have to tell you this, Sir Tantrump, but that makes the whole rest of the world your ENEMY. If it wasn't already.

 

[W.D.Clinger]

OpenAI releases 372 math result groups on GitHub

The 722 papers span number theory, algebraic geometry, and other fields, and include advances related to 3 remaining Millennium Prize Problems

tech.yahoo.com

i was asking about this story.

There are two things going on here.

The proofs themselves appear to have been checked using the Lean programming language. Before editing my previous post, I confirmed that both of the specific proofs I mentioned have been checked using Lean, and that the Lean source code for those proofs is freely available at github. There does not appear to be a great of doubt concerning the correctness of these AI-generated and Lean-checked proofs.

The controversial aspects of this concern (1) attribution of credit, (2) use of mathematicians' work (which is often copyrighted), and (3) the use of open (i.e. unsolved) mathematical problems to test AI models.

Attribution of credit and the use of others' work are issues that have been discussed extensively within this thread, and I don't see why those issues are any more or less important for mathematics than for other applications of AI models.

Using open problems to test AI models is worrisome for several reasons. One is that many mathematicians have spent years making progress toward solving some of those problems, and they understandably resent the possibility that some AI model, building on their hard work, may swoop in at any moment to take the credit for a solution.