Navier-Stokes and Lean

I was working on this week's post on Lean after reading Kevin Hartnett's book The Proof in the Code: How a Truth Machine Is Transforming Math and AI. And then yesterday OpenAI announced a solution to Navier-Stokes, one of the Millennium problems. An incredible accomplishment to say the least. Hours earlier Tristan Buckmaster posted about his progress with Levent Alpöge based on a program started by Diego Córdoba and Luis Martínez-Zoroa, and his interactions with OpenAI. I'm still trying to understand what happened and will write more later but I recommend the Quanta article to get you up to speed.

Lean plays a major role for both projects. OpenAI fully formulated their results in Lean. Buckmaster said they have Lean-verified proofs for the three results they made public but held back on the "blowup for hypo-dissipative Navier Stokes" because the Lean verification has not finished. So it's worth taking a look back.

Leonardo de Moura developed the first version of Lean in 2013 as a Microsoft project for proving code correct. Hartnett tells the story of the people involved in the development of the various versions of Lean capturing the excitements and disagreements. What caught me was the lack of backward compatibility, the definitions and theorems formalized in one version of Lean might break in the next. There was a constant need to get the libraries back up to date until the development stabilized.

The best part of the book focused on some big projects in Lean.

• Tom Hales wanting to convince the world that his proof of the Kepler Conjecture was correct.
• Peter Scholze wanting to convince himself of the correctness of his liquid tensor experiment.
• Kevin Buzzard, Johan Commelin and Patrick Massot formalizing Scholze's Perfectoid Spaces to show Lean can handle modern mathematical objects.
• Terence Tao wanting to formalize in Lean the proof with Tim Gowers, Ben Green and Freddie Manners of the polynomial Freiman-Ruzsa conjecture, just to show it could be done.

None of these were individual efforts but required teams of volunteers to fill in details. Tao approached his proof as a polymath project and his superstar status in the math community really helped get volunteers and popularized Lean.

I did learn a new term from the book, the "de Bruijn factor", the ratio of the length of the formal computer proof to the length of the human proof. I suspect the factor is very large for proofs in theoretical computer science, particularly computational complexity which is why we haven't seen many computer science theorems formalized in Lean.

Hartnett's story ends at the January 2025 Joint Math Meetings in Seattle, a conference I attended. He talks about the initial connections between AI and Lean, but not the uncertain AI future that started to worry mathematicians. By the time the book was published in June 2026, we had seen tremendous progress in AI proving theorems. We've seen even more progress in the three months since, even in the last three days given the news above.

Lean plays a different role now. No longer do you need to write Lean code, any more than you need to write Python code, you can just use AI to generate it. Anthropic fully formalized Fermat's Last Theorem in Lean just last week and hardly caused a stir. 

And now Lean, particularly in Navier-Stokes papers, is being used as a time-stamp, a way to claim your theorem before having to write it up properly in an explainable way. Buckmaster even held back a result because it wasn't yet Lean verified. The way we even publish results is a-changing.

Richard Stearns (1936-2026)

Richard Stearns (right) and Juris Hartmanis in May 1963. The main theorem from their seminal paper is on the blackboard. Stearns sent Lance this picture to help celebrate the 50th anniversary of the paper.

Richard Stearns died on August 29, 2026.  Readers of this blog probably know him from the Hartmanis-Stearns paper On the computational complexity of algorithms which appeared in Transactions of the American Mathematical Society in 1965, and his paper with F. C. Hennie that gave the still tightest known separation for the deterministic time hierarchy.

The Hartmanis-Stearns paper first defined DTIME(T(n)) and other classes and named our field and this blog.  That paper has been honored in two ways:

1) The paper was one of the reasons Hartmanis and Stearns won the Turing Award in 1993.

2) Lance Fortnow chose that paper as one of his favorites, see here.

--------

In this post we discuss a different great paper by Stearns. First some background.

Consider the following problems.

1) Find a function \(f\) such that:

If \(L\) is a regular language and has an NFA of size \(n\) then it has a DFA of size \(\le f(n).\)

(Size is number of states.)

That one we know: \(f(n)=2^n\) suffices.

2) Find a function \(f\) such that:

If \(L\) has a CFG of size \(n\) then it has a PDA of size \(\le f(n).\)

(We assume the CFG is in Chomsky Normal Form and size is the number of nonterminals.)

That one we know: \(f(n)=n+O(1)\) suffices.

3) Find a function \(f\) such that:

If \(L\) is a regular language and has a CFG of size \(n\) then it has a DFA of size \(\le f(n).\)

Meyer and Fischer showed that \(HALT \le_T f\). Beigel and Gasarch later improved this to \(INF \le_T f \) and showed that was tight.

-----------------

Is there any pair of devices such that the gap is greater than exponential but not undecidable?

Richard Stearns in the paper A regularity test for pushdown machines showed the following:

If L is a reg lang with a DPDA of size n then it has a DFA of size \( \le n^{n^{n^{O(n)}}}\)

The size of a DPDA is the number of states plus stack symbols.

Leslie Valiant in the paper Regularity and related problems for deterministic pushdown automata improved this to:

If L is a reg lang with a DPDA of size n then it has a DFA of size \( \le 2^{2^{O(n)}}\).

which matches a lower bound in the Meyer-Fischer paper. Both Stearns and Valiant's results are interesting since the blow up is greater than exponential but still computable.

What is a Computer?

Ben Brubaker has a new Quanta essay Does Computer Science Need Computers? 

Despite the title (and authors generally don't choose their titles), Brubaker's essay really addresses the question as to whether computer science is about computers. He starts with Dijkstra's apocryphal quote "Computer science is no more about computers than astronomy is about telescopes."

This is the wrong analogy: computers are not the telescopes, they are the stars. You just have to use a broad definition of computer.

The word "computer" goes back to at least 1613. The etymology

1. Latin com- meant “together.”
2. Putāre meant “to reckon” or “calculate”—and originally “to prune” or “clear up.”
3. English added -er, meaning “someone or something that performs an action.”

The word originally meant one who computes, usually referring to a human performing a computational task. Its meaning as a machine didn't come into wide use until the mid-20th century. 

I start off every undergraduate theory class I teach with the question "What is a Computer", even in my Foundations of Complexity posts. After some discussion we end up with a diagram like this.

A Computer

The computer doesn't need to be electrical, mechanical or biological. You can think of the postal service delivering a letter based on an address, an auction arriving at a price, or even a well that draws water as we pull a rope. 

The Church-Turing thesis says the process can always be represented by a Turing machine, and then we are off to the races.

When theoretical computer science stops talking about computing, it just becomes mathematics and no longer computer science. If we want to keep it computer science, we need a computer at the center, some kind of process.

How about the title "Does Computer Science Need Computers?" No, not for electronic computers, though they've become more helpful, especially in this AI era. But doing research in computing is a process in itself. Alan Turing drew inspiration for his machine from thinking about how a mathematician works. So yes, you need a computer for computer science, and a computer for astronomy and every other discipline, even if that computer is just yourself.

Claude and Colorblind Questions

BILL: Lance, I have a question and a meta question:

a) List all the presidents and vice presidents who were colorblind.

b) Do you know this sort of thing since you are colorblind, and hence

might have looked this up in the past?

LANCE: (b) No. And if Marco Rubio runs for president in 2028 he will need to earn my vote. He won't get it just for being colorblind. As for (a) I asked Claude.

Only one case is reasonably well documented, and it isn't a vice president. Bill Clinton is red-green colorblind: during the 1996 presidential debates, both Clinton and Bob Dole needed a modified cue-light system, since individual colored lights would have been hard for either of them to read, so a three-light arrangement was used instead — an anecdote that traces back to the Encyclopedia of Genetic Disorders and Birth Defects. Dole, of course, was Ford's running mate in 1976 and lost, so he never made it to the vice presidency.

Eisenhower is the other plausible case. His grandson David wrote that Ike confused browns and greens, sometimes asking for a brown suit when he meant green, and couldn't tell what color his golf balls were — someone had to write "DDE" on them. That's a family recollection rather than a diagnosis, but it's the kind of detail people don't invent.

Everything else you'll find online — Madison, Chester Arthur, Washington failing to distinguish crimson from scarlet, Lincoln calling lavender blue — comes from content-farm pages that cite nothing checkable, and I'd treat it as noise. Lincoln's documented eye problem was strabismus (eyes do not line up), not color vision.

As for vice presidents: I can't find a single one with any credible claim. That's a bit surprising statistically — roughly 8% of men of Northern European descent are red-green deficient, and with fifty-odd vice presidents you'd expect several. The explanation is almost certainly that nobody was looking. Color blindness is invisible unless someone asks, the Ishihara test only dates to 1917, and a nineteenth-century politician had no occasion to disclose it. Clinton's case surfaced only because television lighting forced the issue.

BILL: They left out Hubert Humphrey whose colorblindness was well known and well documented. It was why he was unable to serve in WW II. His not serving was used against him early in his career.

LANCE: I asked Claude about that and here is what it said:

Good catch — that's the vice-presidential case I missed, and it's better documented than anything on the presidential side. Humphrey tried to enlist after Pearl Harbor and was turned down three times, twice by the Navy and once by the Army, on account of color blindness along with other physical problems. Biographical accounts add that he also had a double hernia and lung scarring, possibly from unpasteurized milk.

This one holds up because it left a paper trail: military induction physicals in the 1940s included Ishihara-style screening, so his condition was formally tested and recorded rather than inferred from someone's recollection about suits or golf balls. It also mattered politically — the failed enlistment dogged him, since he was a young man of draft age who spent the war teaching and working for the WPA, and opponents used it against him in his early Minneapolis campaigns.

So the honest tally is one vice president (Humphrey), one president (Clinton), plus Eisenhower as a plausible unconfirmed case. Which, incidentally, undercuts the "nobody was looking" explanation I gave a moment ago — the real filter was that the condition surfaces only when an institution forces a test, and the military did that for exactly the cohort of politicians who came of age around the world wars.

BILL: SO, why did it get it wrong? This is not something  obscure which requires guesswork like speculating on whether Washington was colorblind (I can't tell scarlet from Crimson either).

LANCE: Google AI did even worse.

BILL-AI can solve Erdős problems, but it can't track down that Hubert Humphrey was colorblind. Why is that?

LANCE- Claude was just too lazy to check over the military records of every vice-president. AI are people too!

The Calculator Transition

There's a scene in Apollo 13 where Jim Lovell, played by Tom Hanks, asks Houston control to check his calculations, which they do using a slide rule. 

My father told me that when he was in college (1950s) that engineers measured their technical prowess in how many digits of accuracy they could get off a slide rule.

The actual Apollo 13 incident took place in 1970. A year later Bowmar/Ali released the 901B, nicknamed the Bowmar Brain, for about $240. 

The following year came the HP-35, the first successful handheld scientific calculator that put slide rules out to pasture.

A couple of years later I asked for a calculator for my birthday (the math nerd I was). I insisted on it having a memory button that could remember one number so I could do more complex calculations. The one I got even had a square root button!

By the time I got to high school at the end of the decade, we all had handheld calculators. My AP chemistry teacher still insisted on teaching us how to use a slide rule. For fun, I decided to use my father's slide rule on a chemistry exam. That was a mistake for two reasons.

1. I did not have the "technical prowess" to get many digits of accuracy. So especially after a few calculations, my numbers were way off. The teacher took pity on me and gave me credit because I had the formulas right.
2. I spent too much time doing the calculations where everyone else just punched numbers into their calculator and didn't finish all the problems. 

Maybe with more experience I could have handled both issues better, but that was the last time I used the slide rule for any important calculations. School children still learned how to add and multiply, but I'm not sure my kids can do long division. Certainly I was the last generation to learn how to do square roots by hand.

Is there an AI lesson in all this? We went from slide rules in mission control to calculators in high school in under a decade. No one suggests we go back to slide rules, and using a slide rule is now a lost art. Civilization survived.

But there's a bigger story. The slide rule and calculator took care of the routine math, but the teacher graded me on my knowing the Chemistry. AI Can now do the chemistry. And what's left after that?

Centaur Math

In the past, new PhD students would ask how they could succeed when they had to compete with the likes of say, Richard Karp or Avi Wigderson. I would say Karp and Wigderson have limited bandwidth and you can work on problems they don't work on, or think deeper about a problem than Karp or Wigderson has time to.

Now we get the same question but with names like Claude and ChatGPT and it's hard to make the same bandwidth argument. What do we tell them as we get closer to Math AGI?

What even is Math AGI? It's not that every math problem gets solved. I don't expect P vs NP to be solved anytime soon. It would require a completely new approach, and AI doesn't (yet) think outside the box, though it has a very large box.

Math AGI means that with rare exceptions, if AI can't solve a math problem then no human could either. If you need a proof, you'd have to pay for more cycles, or wait for the next new and improved model. Like the Turing test, we'll only truly realize we've reached Math AGI once we've gone well past it.

We haven't reached Math AGI yet and we may never fully get there. We have entered the world of Centaur Math. Mathematicians can still prove theorems AI can't, AI can prove some theorems mathematicians haven't yet proven, but the real strength comes with mathematicians and AI working together. Working with AI today is like having a pretty good PhD student, who has a huge broad base knowledge of mathematics, is a whiz at coding, but still needs direction, encouragement and verification.

Chess had a short centaur moment when humans and AI working together could beat the best human players and AI programs. Now, any human would play worse not following what AI says. Nevertheless, we still enjoy watching two sub-AI humans play chess against each other. I doubt the same would hold for sub-AI mathematicians.

So what do we tell the students? If you love math, do math. Embrace AI, use it to go further, not as a crutch. Challenge yourself and remain agile so you can find success whatever the future might hand us. And remember, math is not ultimately about the theorems we prove but how we understand the principles behind them, and that's a human endeavor not a machine one.

IIT is the canary in the coalmine (Do our younger readers know what that means? Do we have younger readers?)

Lance has posted about his, and around 160 others, being laid off from IIT here.(IIT stands for Illinois Institute of Technology which is where Lance was employed.)

Hence I looked into what is happening at IIT to see if there is a lesson for us all.

I) I wondered why IIT had declining enrollment. I wondered which of the two reasons below  was the issue (and of course there are other reasons). 

--The enrollment cliff.  (See here)

--International students have declined in number. Why? (1) Having getting student visas, (2)  They think they are not welcome here (3) Schools in their home country getting better. Note that I am just guessing.

Rather than speculate I asked ChatGPT for the data on both enrollment and on international enrollment from 2015 to 2025. Here is the data: here.

a) 2015 had an enrollment of 7792. It went down in 2020 (COVID?) but then came up again and it was 8838 in 2024.  In all the years for which there is data international students were about half of the students.

b) 2024: 8838 students, of which 4596-International (52%), 4242-Americans

   2025: 7502 students, of which 2141-International (42%), 5361-Americans

So it looks like the enrollment cliff was not a problem since more Americans came, but the decline in international students is a problem.

I think that international students pay more, so their decline creates more of a financial pinch.

----------------------------------

II) I wondered if other schools had massive layoffs so  I asked Google AI what other schools had laid off more than 30 professors in the last two years. It had an issue with that since schools combine faculty and staff.  Even so, the main fact is that (a) it is happening at other schools, and (b) 160 is more than usual. 

--------------------------------------

III) Challenges facing Universities

a) The enrollment cliff. This will be a real problem for small schools.  For big schools it may be an opportunity to have smaller classes.  This issue cannot be stopped.

b) Less international students means less money. This may change since this or a later administration may change the rules. However, changing the rules might not help much since other countries have fine schools and international students may feel they are not welcome here.

c) Grants are drying up. Again, this may change.

d) AI and cheating. This may make us rethink the entire point of education.

e) Does college exist to create an educated public who can make decisions and vote intelligently, or are colleges vocational? It's getting harder to do both.

f) Fads: The hot topics in CS now are Quantum, ML, and Quantum ML. What will they be in 10 years?How do we adjust? Do other fields have this problem? ML (or more broadly AI) is hot in that students want to take it because it both sounds interesting and sounds employable. Quantum is hot for grant money and some students think its going to be cool. (In this context `Hot' and `Cool' are not opposites.) 

g) Tuition keeps going up. The business model may be broken.

h) A while back online education seemed like it might be an alternative for some students (MOOCS were hot). That hasn't happened yet but it might.

i) This is a far bigger subject than the points above. Maybe Lance can write a book on the topic now that he has some free time.

Unexpected Unemployment

Enjoying Idaho while ignoring Illinois

Today is the first day of my life that I am unemployed. And not by choice.

As I mentioned on LinkedIn last week, me and about 160 of my colleagues, staff and faculty, untenured and tenured, lost our positions at Illinois Tech after they declared "financial exigency" which allows them to eliminate tenured positions. I'll use this post to tell my story, but keep in mind there are 160 other ones.

The president announced that he would be asking the board to declare financial exigency in mid-July so we knew layoffs were coming but not when. On July 25th, we left for a planned 12-day vacation to Idaho. Why Idaho? It's my fiftieth state, so my wife and I decided to make a vacation of it. We saw Boise, canyons, craters, mountains, lakes. We were in Twin Falls three days before a mass shooting but that's a different story.

Usually I avoid reading work emails on vacation but decided I probably should this time. And on day four of vacation, I got an email invite to a meeting with the Vice-Provost of Faculty Affairs and an HR representative titled "Organizational Update" and I knew my fate was sealed. By the next day I was tired thinking about it and just decided to enjoy the rest of the vacation and deal with everything when I got back last Thursday. It might have been better if I simply didn't read email like usual.

It really hit me as I started to pack up my office Monday, for the first time with no office on the other side. Monday was also the first day of orientation week and a group of new students walked by as I was packing boxes into my car, though I don't think they noticed.

Illinois Tech got hit hard by a large drop in foreign graduate enrollment due to changing visa requirements, general anti-US sentiment, more opportunities in other countries and a weaker job market for graduating Masters students partly due to artificial intelligence. Universities face challenges beyond international students including Baumol's disease, administrative bloat to meet expanding regulations, the demographic cliff, reduced grant funding, and less support of universities by the public and both political parties, and AI changing how and why we teach. Illinois Tech is one of the first tech research schools to eliminate tenured roles, but it won't be the last.

I'll be okay but many of the other faculty could really use another position, in some cases so they can stay in the US. If you have opportunities for faculty in any discipline, let me know and I'll pass it along.