Theory and Practice in the Age of AI

In the last week folks at OpenAI submitted a resolution of the Millennium prize problem on the singularities of the Navier-Stokes equation. This was a problem that had been open for a while against the best humans could offer, and the folks at OpenAI purportedly solved it with an agent swarm. This seems to have been done with agents trying approaches with automated proof verifiers. At a high level, they had an agent take several directions of attack on a problem, and break each attack into a bunch of sub-problems that need to be solved, and have an agent trying to solve the subproblem. This is just getting a program to compile in the formal language of the proof verifier (sort of analogous to getting an agent to get a program to compile). Then they had checkpoints where the approaches which were most promising were assigned more agents to work on them. Using this, they solved it in 88 hours with a 10,000 agent swarm.

Like many others, this event shook me to the core as well. I am trying to jot down my thoughts here. There has been a lot of discussion and introspection around the future of math and academia – including the announcement of the creation of The Association for Human Mathematics, a petition from academics including 25 Fields medallists on the place of AI in math, and the editor-in-chief of arXiv lamenting the proliferation of preprints where the authors do not seem to understand the papers they author. While there is a lot of interesting discussion in those directions, I am more interested in the possible implications for engineering – in both theory and practice, in academia and industry.

A Paradigm Shift

In Engineering, we generally get to theory problems from applications. For example Claude Shannon came up with A Mathematical Theory of Communication when he was thinking about how one can design a system transmitting information from one point to another. This theory was rich enough and the problems involved were hard enough, that many smart people spent around 60-70 years to resolve and solve. The paradigm has been: practitioners come up with problems to come up with better designs for engineering problems, and that gives academics a rich theory to build on. The practitioners benefit from these academic advances and are able to come up with better designs – over a long timeframe like a decade or more.

With LLMs acting in tandem with proof verifiers, I think solving well-specified theory problems relevant to engineering will largely be much easier. This is going to force a paradigm shift, both in industry and academia.

In academia, I don’t think it will be viable for engineering faculty and grad students to do purely theory work. Most theory problems that engineering practitioners are interested in are not of the sophistication/hardness of the Millennium problems. LLMs will probably be handy at making a lot of progress at these problems; if not solve them outright. However the best engineering grad students are in doctoral programs for being creative and not just sit by (almost) magical theorem provers. To do this, grad students and faculty would have to do at least some work LLMs cannot do as of now. That is, almost all engineering grad students/faculty will have to do less solving of well-specified theoretical problems, and do more modeling, formulating problems, running experiments, and building systems. (This is quite painful for me to say being a theorist in grad school.)

In industry, usually theoretical problems are “outsourced” to academia because of resource constraints. Sub-optimal designs are usually good enough; and companies who build products do not see economic sense in having productive people spend months on solving some theoretical problems which will make designs a bit better. However, now with the LLM-theorem-verifier loops practitioners have the ability to in-house this process (and as a practitioner with time constraints, one is happy to have a LLM help prove a theorem). Going forward, I see more and more practitioners come up with better designs because they can solve theory problems internally. One sad third-order effect is we will have fewer theory-solving engineering problems published openly, as practitioners care more about working products than papers (Even if there is no desire to keep things closed source, writing a paper well requires significant effort and there is no incentive for companies to allocate resources for that.)

Similar to the situation in industry, this will also make theory more accessible to experimentalists in academia, which will lead them to in-house a lot more theoretical work as well.

Lean into Automated-Theorem-Provers

One aspect that has drawn considerable amount of discussion has been using automated theorem provers like Lean to generate proofs. These proofs are formal proofs of statements (modulo bugs in the theorem verifiers), which by themselves are not of much help to engineers. Usually insight comes from looking at ideas in converses or constructions in achievability results in the proof, not from whether a theorem is true or false.

Having said that, I think automated theorem provers will be very useful with LLMs both in academia and in industry. The main time sink I have found when working on theory is that progress is bursty, that is, I make some progress and then get stuck for a while and then make some progress after a few days perhaps. LLMs and automated theorem provers let us cut short the amount of time we’re stuck while working on theory problems, which I think will be invaluable. (I’ve been learning Lean, and it’s fascinating)

Concluding Remarks

While we’re unquestionably at a place where the way research is going to be done is going to change significantly, I think the ability to prove theorems easily using LLMs and theorem-verifiers is going to increase the amount of theory done in industry, and among engineering academics make theorists do more experimentation and modeling, while enabling experimentalists to do more theory.

As with any prediction, I could be completely wrong. But it is undeniable that we’re living in exciting times.