Elektrine lite

← Feed

@scruiser@awful.systems

2026-10-10 03:17 UTC

Lean and Autoformalization: some helpful links 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!

Replies (6)

  • @o7___o7@awful.systems 2026-10-10 06:51

    Thanks for putting this together in one spot!

    Open ##4971458

  • @blakestacey@awful.systems 2026-10-10 17:54

    After the paper was written, the author learned that the same result was also proved independently and by a different method by Ningyi Li [7]. The result is also contained in a paper [8] released by OpenAI on October 6, 2026, in which the proof strategy and specific choices of notation are identical to a preliminary version of the present paper that was uploaded to ChatGPT on September 8, 2026. uh-oh spaghetti-o

    Open ##4975979

  • @EFreethought@awful.systems 2026-10-10 19:10

    I have looked at a few comment threads about the math proofs on Hacker News. I only got as far as business calculus about 30 years ago, so some of it was beyond me. I noticed that some commenters have no problem with the fact that a lot of the proofs are almost incomprehensible to humans. I do not see the point of math for AI alone, since I do not think AI is or will ever be conscious. It is another example of people thinking that our lives should be not just pro-AI, but AI-centric. To them, the AI is not here for us, but we are here to serve the AI.

    Open ##4976828

  • @blakestacey@awful.systems 2026-10-11 01:00

    Thread: bsky.app/profile/…/3mxeqyegazk2h

    Open ##4980142

  • @Amoeba_Girl@awful.systems 2026-10-11 09:09

    It’s really fucking me up the way AI boosters and friends are treating mathematics as a natural science whose goal is to uncover mathematical facts in the number mines. I’m not even staunchly opposed to platonism, but my god. That’s not even how natural science works! Random idiot on r/singularity That stance assumes we still need to fully understand the manual mechanics in order to apply the end result. ​Saying we lose out on the “journey” is like an 18th-century laborer complaining that the steam engine will create a society where no one has the endurance to swing a 20-pound hammer for a full 12-hour day. Do we lose something through abstraction? Absolutely. And I understand why people would mourn that. But do we need to have the endurance to swing the hammer to build a modern skyscraper? ​>We aren’t losing the ability to do math, we are just moving up a layer of abstraction, transitioning from the laborers to the architects. Also look out for the new obnoxious metaphor of “what if aliens descended from the sky and handed us their science and proofs, how is this different”. First of all shut up. Secondly we should assume the aliens in this scenario have reason, intent, and the ability to communicate through language. You’re imagining they’re using the scientific method and not divination from wiggling their proboscis in the fourth dimension. Which is quite different from OpenAI’s big dump on scientific practice.

    Open ##4984587

  • @EFreethought@awful.systems 2026-10-11 16:16

    Here is a video I came across today that seems relevant to the discussion: www.youtube.com/watch?v=KqiDqJMxg6o He is a professor at Imperial College in London. He says that a potential negative consequence of having AI do the math is that if people stop doing it, then there will not be enough people to understand and check the math and to push back against bad proofs. A few years ago I was at the local Java meetup and the speaker was from Azul Systems. They contribute to OpenJDK, offer support contracts, and I think they used to make a special JDK for embedded systems. He said there is a big sign at one of their offices that said: “We write in C, so you don’t have to”. I took enough C to understand what things like the JDK or the Golang runtime are doing for me wrt things like memory management. I do not know a lot about C, or anything about the C compiler, or the assembly, or the chip, or all the layers underneath. But I do know that there are people who do know that. The point of all that is: What if we wind up in a world where nobody understands how the JDK or other runtimes work anymore? Or if the only people who do use their knowledge to break or take down systems running one of these runtimes? That is where I think things are heading. We started this decade with doors falling off of airplanes, and a lot of people seemed to think that is a wonderful idea.

    Open ##4989085