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

Post by DiscourseFan » Sat, Jan 10, 2026, 3:52 PM UTC

frozenseven wrote: post #295

DiscourseFan wrote: post #152

Earlier quoted context omitted.

It requires constant feedback, critical evaluation, and checks. This is not AGI, its cognitive augmentation. One that is collective, one that will accelerate human abilities far beyond what the academic establishment is currently capable of, but that is still fundamentally organic. I don't see a problem with this--AGI advocates treat machine intelligence like some sort of God that will smite non-believers and reward…

>AGI advocates treat machine intelligence like some sort of God that will smite non-believers and reward the faithful. >The real world is not composed of rewards and punishments. Most "AGI advocates" say that AGI is coming, sooner rather than later, and it will fundamentally reshape our world. On its own that's purely descriptive. In my experience, most of the alleged "smiting" comes from the skeptics simply being wr…

Post by jacquesm » Sat, Jan 10, 2026, 4:07 PM UTC

Mawr wrote: post #312

jacquesm wrote: post #296

Earlier quoted context omitted.

And none of those details matter to solve the problem correctly. I'm purposefully not putting any answers here because I want to see if future generations of these tools suddenly see the non-obvious solution. But you are right about the fact that the details matter, one detail is mentioned very explicitly that holds the key. If you do solve it don't post the answer.

Sure they, do, the problem makes no sense as stated. The solution to the stated problem is to remove all weights all at once, solved. Or even two at a time, opposite the centre of gravity. Solved, but not what you're asking I assume? You didn't even label your ASCII art, so I've no clue what you mean, are the bars at the end the supports or weights? Can I only remove one weight at a time? Initially I assumed you mean…

Post by kittikitti » Sat, Jan 10, 2026, 4:31 PM UTC

Post by fsmv » Sat, Jan 10, 2026, 4:58 PM UTC

oh_my_goodness wrote: post #326

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…

>That's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Sure. But it's fair to ask how to validate that assumption.

Post by Jweb_Guru » Sat, Jan 10, 2026, 5:03 PM UTC

ndriscoll wrote: post #179

mjevans wrote: post #173

Earlier quoted context omitted.

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

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.