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

Post by red75prime » Sat, Jan 10, 2026, 10:27 AM UTC

varjag wrote: post #269

red75prime wrote: post #256

Earlier quoted context omitted.

I suppose there's no formally defined procedure that accepts a natural language statement and outputs either its formalization or "misspecified". And "absolutely true" means "the vast majority of mathematicians agree that there's only one formal proposition that corresponds to this statement".

I think you suppose wrong. A statement like "the area of the square whose side is the hypotenuse is equal to the sum of the areas of the squares on the other two sides" doesn't seam out of reach of an algorithmic procedure like a classical NLP.

Post by davidwritesbugs » Sat, Jan 10, 2026, 10:36 AM UTC

heroprotagonist wrote: post #252

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…

Soo, it can definitively tell you that 42 is correct Answer to the Ultimate Question of Life, The Universe, and Everything. It just can't tell you if you're asking the right question.

Post by latexr » Sat, Jan 10, 2026, 11:00 AM UTC

feastingonslop wrote: post #131

falcor84 wrote: post #125

Earlier quoted context omitted.

> Any talk of "AGI" is, as always, ridiculous. How did you arrive at "ridiculous"? What we're seeing here is incredible progress over what we had a year ago. Even ARC-AGI-2 is now at over 50%. Given that this sort of process is also being applied to AI development itself, it's really not clear to me that humans would be a valuable component in knowledge work for much longer.

Excellent! Humans can then spend their time on other activities, rather than get bogged down in the mundane.

Post by falcor84 » Sat, Jan 10, 2026, 11:01 AM UTC

DiscourseFan wrote: post #152

falcor84 wrote: post #125

Earlier quoted context omitted.

> Any talk of "AGI" is, as always, ridiculous. How did you arrive at "ridiculous"? What we're seeing here is incredible progress over what we had a year ago. Even ARC-AGI-2 is now at over 50%. Given that this sort of process is also being applied to AI development itself, it's really not clear to me that humans would be a valuable component in knowledge work for much longer.

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…

Post by tomjen3 » Sat, Jan 10, 2026, 11:07 AM UTC

maxwells-daemon wrote: post #166

aidenn0 wrote: post #148

Earlier quoted context omitted.

How do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible sounding lies, so I'm wondering how likely that is for this usage.

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!