“Erdos problem #728 was solved more or less autonomously by AI” • Hacker News Board

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

#381

Post by falcor84 » Mon, Jan 12, 2026, 3:06 AM UTC

zeroonetwothree wrote: post #320

falcor84 wrote: post #300

Earlier quoted context omitted.

Yes, absolutely willing to commit. I can't find a single reliable source, but from what I gather, over 70% of people in the West do "pure knowledge work", which doesn't include any embodied actuvities. I am happy to put my money that these jobs will start being fully taken over by AI rapidly soon (if they aren't already), and that by 2035, less than 50% of us will have a job that doesn't require "being there". And re…

I would easily take the other side of this bet. It just reminds me when everyone was sure back in 2010 that we’d have self driving cars within 10 years and human drivers would be obsolete. Today replacing human drivers fully is still about 10 years away.

Yes, getting the timelines right is near impossible, but the trajectory is clear to me, both on AI taking over pure knowledge work and on self-driving cars replacing human drivers. For the latter, there's a lot of inertia and legalities to overcome, and scaling physical things is hard in general, but Waymo alone crossed 450,000 weekly paid rides last month [0], and now that it's self-driving on highways too, and is slated to launch in London and Tokyo this year, it seems to me that there's no serious remaining technical barrier to it replacing human drivers.

As for a bet, yes, I'd really be happy to put my money where my mouth is, if you're familiar with any long bets platform that accepts pseudonymous users.

[0] https://www.cnbc.com/2025/12/08/waymo-paid-rides-robotaxi-te...

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

#382

Post by mikhailfranco » Mon, Jan 12, 2026, 8:14 AM UTC

kovek wrote: post #344

svat wrote: post #339

Earlier quoted context omitted.

It may help to look at this example concretely: The natural-language statement of the problem is (from https://www.erdosproblems.com/728 ): > 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? The Lean-language statement of the problem (which can be done either by hand or by AI) is (from https://github.com/plby/lean-proofs/blob…

I'm wondering how do people come up with these mathematical challenges?

Live out of a suitcase, travel the world, hang out with a wide selection of excellent mathematicians, write joint papers with many of them, when you get bored or stuck, pack the suitcase and keep moving - for your whole life.

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

#383

Post by oh_my_goodness » Mon, Jan 12, 2026, 1:34 PM UTC

ndriscoll wrote: post #369

oh_my_goodness wrote: post #328

Earlier quoted context omitted.

Everyone has a different perspective, based on their math background. From the OP's perspective, the formalization of this problem statement was apparently worth talking about. On the other hand, for you it's just a homework problem that belongs in an intro class. Let's just be generous and try to accept these differences.

My comment was exactly about the required math background though. Anyone who's completed an intro to proof class would find that kind of statement easy to formalize because they would have had to write similar statements for homework. That provides some context: everyone who's interested in computer theorem provers probably has some experience with proofs, so formalizing that statement should be easy for them. i.e. (…

I think it's reasonable to ask whether LLMs formalize theorems correctly. And I'm not sure that saying "this one is easy" answers that question.

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

#384

Post by kelipso » Mon, Jan 12, 2026, 4:07 PM UTC

ogogmad wrote: post #378

kelipso wrote: post #315

Earlier quoted context omitted.

I’m going to replace every instance of 1 with 0.999 repeating, do the equivalent for all all integers, and see how my mind totally explodes.

?

I thought we were all doing jokes, no?

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

#385

Post by eab- » Wed, Jan 14, 2026, 12:49 AM UTC

roadside_picnic wrote: post #54

sublinear wrote: post #23

Earlier quoted context omitted.

I agree only with the part about reconfiguring existing proofs. That's the value here. It is still likely very tedious to confirm what the LLMs say, but at least it's better than waiting for humans to do this half of the work. For all topics that can be expressed with language, the value of LLMs is shuffling things around to tease out a different perspective from the humans reading the output. This is the only realis…

> It is still likely very tedious to confirm what the LLMs say, A large amount of Tao's work is around using AI to assist in creating Lean proofs. I'm generally on the more skeptical side of things regarding LLMs and grand visions, but assisting in the creation of Lean proofs is a huge area of opportunity for LLMs and really could change mathematics in fundamental ways. One naive belief many people have is that proof…

> We have proofs that are gigabytes (I believe even terabytes in some cases) in size, but we know they are correct because they check in Lean.

I'm not aware of any of these. There's some SAT-like results that were not verified in Lean at that sort of scale, but Lean proofs of individual problems are nowhere near that. For example, Mathlib (think a Lean4 math stdlib) is 6GB including compilation artifacts, and iirc <100MB text.