TechTakes

2733 readers

117 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 6 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

[–] Amoeba_Girl@awful.systems 7 points 5 days ago (1 children)

also maths are not a science there i said it

[–] scruiser@awful.systems 8 points 5 days ago

Someone on Scott Aaronson's blog suggested math will become an empirical field now, where they run "experiments" by asking AI for lean proofs.

Scott, is this a turning point where mathematics gets off its well trodden path of logic and becomes more like an empirical science? Heck, people were arguing if math is invented or discovered, this settles it. Math is discovered – by AI! From now on forth, Mathematicians will become scientists, wielding AI as a telescope, pointed towards new and disturbing alien worlds in the Platonic realm.

So yeah, it seems like this idiotic view is pretty popular among boosters.