27

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:

And some other related links:

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
[-] EFreethought@awful.systems 8 points 22 hours ago* (last edited 22 hours ago)

Here is a video I came across today that seems relevant to the discussion: https://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 going into math, then there will not be enough people to understand and check the math proofs from AI 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.

this post was submitted on 10 Oct 2026
27 points (100.0% liked)

TechTakes

2725 readers
55 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