Remix.run Logo
▲ yewenjie 2 hours ago

> Experience has shown that, even now, there will still be people explaining in patronizing tones why none of this is real and none of it counts. If such people were capable of being impressed by anything that happens in the empirical world, of updating on anything, they would’ve already been impressed and already updated several years ago, long before things had reached the point of an actual Mathocalypse.

^^ half of the comments on this thread

▲ssfdg 2 hours ago | parent | next [-]

Also a ton of comments in this thread: breathless frothing hype declaring mathematics is over and assuming these proofs are exactly what they claim they are at face value, giving the company with a vested interest in everyone unquestioningly believing this is all real every conceivable benefit of the doubt

▲azan_ 2 hours ago | parent [-]

Didn't top math researchers call AI progress absolutely real and dangerous for math? It's not just HN commenters that are impressed!

▲ssfdg 2 hours ago | parent [-]

By all accounts the "dangerous for math" claims seem to be primarily around flooding the field with complicated impossible-to-understand proofs that according to recent research may or may not be correct depending on what's going on with the Lean implementation.

It's looking to me like it's more of a slop PR problem than it is that these things are genius at math and will displace mathematicians. I am happy to be wrong but I strongly suspect the next few weeks to months will result in more and more of this work being exposed as slop.

These things are ok-ish to halfway decent at coding tasks with a ton of babysitting and still make tons of extremely simple errors almost constantly, why should math be any different?

▲azan_ 37 minutes ago | parent [-]

Yes, Lean verified proofs could be wrong, but the chances for that are much smaller than human not spotting error (in absence of formal verification). IIRC the main concern that Tao voiced are indeed impenetrable proofs that humans won't understand, but not concerns about truthfulness (I might have missed something though, so if he or other Fields medalists have talked about that recently I'd be grateful if you could link it).

> These things are ok-ish to halfway decent at coding tasks with a ton of babysitting and still make tons of extremely simple errors almost constantly, why should math be any different?

1) AI is winning programming competitions, 2025 was probably the last year we've had human participant winning* 2) Math is different because there's formal verification.

* Of course competitive programming is different than enterprise programming, but competitive programming is closer to math.

▲Fraterkes 2 hours ago | parent | prev | next [-]

Having stuff explained to you in patronizing tones? How horrible Scott!

▲Rover222 2 hours ago | parent | prev | next [-]

more like 3/4 of the comments but yea

▲ an hour ago | parent | prev | next [-]
[deleted]
▲12kajh 2 hours ago | parent | prev [-]

[flagged]

▲azan_ 2 hours ago | parent | next [-]

You know, if you attack ad personam you've got to be ready that someone will do same against you - what progress did you make in the last 10 years (or in your entire life for that matter)?

▲jamiek88 2 hours ago | parent | next [-]

He was created 14 minutes ago, give him a break!

▲ an hour ago | parent | prev [-]
[deleted]
▲moffkalast 2 hours ago | parent | prev [-]

Trust me bro, just 100 more cubits, I swear we'll break everyone's encryption and cause the downfall of society, please bro just one more grant, It'll be stable this time :'(

▲sebzim4500 an hour ago | parent [-]

Scott Aaronson is best known for being the one calling those guys out, so it's a weird criticism to make here