Post

I had rather stupidly assumed that they’d write the problem statement in lean, and then ask the chatbot to fill in the blanks without using `sorry`, because how else could they trust the result? Turns out they just cross their fingers real hard and smother any ethical feelings with a wad of cash 🫩

This is quite a basic (complementary) observation about agents, but you'd expect them to produce a much higher rate of compiling proofs compared to working arguments since the former is a determinate signal fed to the agent for it to optimise for

Some of these Lean proofs are millions of lines long. So what OpenAI is doing is presenting a "result" that may or may not be the same as a huge git repo of Lean files. The paper demonstrates examples of incorrect proofs being "translated" into correct Lean by GPT!

I feel like this is to OpenAI's benefit. It is good publicity that can't really be (dis)proven until months later when people have moved on and it helps them further sell the idea that only they can do these immensely complex proofs because how are we to know if a real proof is way simpler

Why review it yourself when you can just dump the labor of reviewing it onto the people you're trying to replace and have them do the work for free? Dumping piles of possible shit for humans to review is kinda their whole MO.

The cynic in me would say it's because the goal is not to solve the problem or find the proofs. The goal is to sell the idea that AI is waaaay better than people, so why don't you just use it instead of the slow, messy, emotional, family and illness having meatsacks? Do you want to get left behind?

The rest were useless or wrong or fake or *scraped from actual human-made bug reports*. 26,000 sounds impressive and gets news articles written about it. The follow-ups whittling that number down ... don't. And I think the AI companies exploit this. More info here: pivot-to-ai.com/2026/10/07/m...