blakestacey comments on Lean and Autoformalization: some helpful links

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

submitted 5 days 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 4 days ago (1 child)

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

permalink

fedilink

source

hideshow 1 child comment

[–] scruiser@awful.systems [S] 2 points 4 days ago* (last edited 4 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".

permalink

fedilink

source

parent