Lobsters: After Math

In the very long term, I see programming going in a similar direction as math

There will be increasing value in a good presentation and a good program/proof -- for humans to understand. Elegance and readability will count.

As a thought experiment, if you suppose AI is infinitely good and infinitely cheap, then eventually you will want to use it to rewrite the program in a way that's more legible. And that will probably mean developing new notations and new programming languages

I still think of programming in the large as the problem a trillion dollars can't completely solve. If you look at say Windows and OS X, I'm sure everyone who works on them recognizes their decline in quality. But they have a trillion dollars and they can't really do much about it

I mean likewise with Linux -- nobody would claim it's optimal; it's just very useful and better in many dimensions than the alternatives. I still think the true test of AI is whether it moves the needle of any of these things

e.g. similar to "why are there 5k+ issues open on CPython and 5k+ issues on Rust". Because the bottleneck is human design and understanding, and that will continue to be the case indefinitely.

It's a lot easier to apply AI to problems/programs that nobody cares about than ones that millions of people (and computers) depend on

People need to adjust themselves to what problems they are able to solve that AI cannot.

I'm not sure this engages with the article's content, e.g.

In mathematics, it is more natural to treat AI as an assistant rather than as a competitor. As Jeremy Avigad (2026) puts it, “We should keep in mind that AI is nothing more than technology, designed to serve our purposes. It is misguided to think of mathematicians as competing with AI; when we drive a car, we aren’t competing to see who can go faster, and when we use a phone, we aren’t competing to see who can speak louder.”

and

We do not deny that, if OpenAI’s announcement is correct, this is an extraordinary achievement. But we should get clear about what type of achievement it is. At this moment, it is an answer, not a solution. And, even if in time the result reveals itself as a genuine solution, we have argued that, in the practice of mathematics, solutions are not everything.

etc

Concretely, is AI going to propose 7 new millenium problems? Or will people not care? What about Erdos conjectures?

A concrete answer is hard at the moment, I think it is still not clear where all of this is going, even though the recent field medalists petition and the Leiden declaration are setting a path to figure it out.

So far I think LLMs have been advantaged by the improvements in formalised mathematics and it is a good way to “show off” and get marketing noise out. I don’t see any of the model having any kind of insight suitable to set what the new millennium problems will be.

Usually these are the result of deep understanding, which comes from having worked, studied and struggled with the problem long enough, and I think is also one of the points of this post (and many others popping up). I don’t expect this to change.

But AI as a tool I feel is growing fast, and certain problems, where there is enough literature scattered throughout many years, are better suited for being solved by LLMs. Many Erdös problems follow in this category for instance

As another thought experiment: Is AI going to be able to propose, design, and implement new languages like Lean and Coq autonomously?

As I understand it, these languages are doing a lot of the heavy lifting -- the AI can brute force the search space (with often surprising intuition/insight), and if it passes Lean, then the theorem is proved. (And then people need to go back and figure out WHY it's true)

Right now, I doubt it -- I suspect any successor to say Lean will be done by humans and AI to collaborating. The relationship is complementary in many ways -- framing it as either/or is misleading.

The AI labs should try to solve BB(7).

The fun part about solving BB is we will run into a computational bottleneck or an intelligence bottleneck. There is no scenario where BB gets solved.