TechTakes

2735 readers

235 users here now

Big brain tech dude got yet another clueless take over at HackerNews etc? Here's the place to vent. Orange site, VC foolishness, all welcome.

This is not debate club. Unless it’s amusing debate.

For actually-good tech, you want our NotAwfulTech community

founded 3 years ago

MODERATORS

dgerard@awful.systems

Lean and Autoformalization: some helpful links (awful.systems)

submitted 1 week ago by scruiser@awful.systems to c/techtakes@awful.systems

17 comments fedilink hide all child comments

So the boosters are making a big deal about the dump of "proofs" OpenAI has made recently, so I thought I would collect some relevant links in one place...

Stuff on autoformalization:

A short blog post breaking down some of the bugs found and potential for more
preprint discussing the problems with natural language to lean in detail and pointing out some blatant inconsistencies in the recent Navier-stokes "proof"
/r/betteroffline discussion of above preprint
Some of our very good friends are aware of the problem! Of course, this is lesswrong, so there is a tinge of "this is why we need to be careful with using this sort of approach to make our AI God".
The soundness bug that led to the fallacious disproof of the Collatz Conjecture

And some other related links:

OpenAI already retracting a few papers

Let me know in the comments if you have any links I should to these lists!

you are viewing a single comment's thread
view the rest of the comments

[–] blakestacey@awful.systems 4 points 1 week ago (1 children)

Thread: https://bsky.app/profile/gro-tsen.bsky.social/post/3mxeqyegazk2h

[–] scruiser@awful.systems 2 points 6 days ago* (last edited 6 days ago)

The theory on the thread that

My guess is that this represents a shift in focus at OpenAI away from math: they had their big meaningless trophy prize with the Navier-Stokes solution, they appear to have distanced the competition (Anthropic) and the public bought the notion that “math is solved”

seems like a plausible explanation? I'll guess we'll if OpenAI moves on now that they've "solved" math or if they follow up with a few more drops of "proofs".