▲ 28 ▼ 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!
[–] Amoeba_Girl@awful.systems 7 points 1 week ago (1 child) also maths are not a science there i said it permalink fedilink source parent hideshow 1 child comment replies: [–] scruiser@awful.systems [S] 8 points 1 week 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. permalink fedilink source parent
[–] scruiser@awful.systems [S] 8 points 1 week 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. permalink fedilink source parent