What is the points of AI-disclosure?

The STOC conference (and likely others) are requiring that a submission says how much AI was used. I can imagine the following options:

1) AI was used for proofreading and tightening prose (I think in this case you do not need to disclose).

2) AI was used to shorten the proofs.

3) I came up with the questions but AI supplied all of the answers.  However, I have read it and take responsibility for the content.

4) AI came up with the questions and AI supplied all of the answers.  However, I have read it and take responsibility for the content.

It is my understanding that whether you say 1,2,3, or 4 it will not be held against you in deciding whether STOC accepts or rejects the paper.  (Please correct me if I am wrong.) This is good in that people will have no reason to lie about their AI-use.

But that raises the question:

Why does STOC require disclosure of AI use?

What is someone supposed to do with that information? If the answer is nothing then I am still puzzled about why we collect it.

When I have a question like this I ask Gemini. Here is what it said and my comments on it.

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

AI Overview

The STOC (Symposium on Theory of Computing) conference, following broader ACM guidelines, requires the disclosure of substantive AI use to ensure transparency, accountability, and credit attribution in scientific research.

BEGIN BILL:

Transparency---That seems circular. We want to know if AI was used to see if AI was used.

Accountability---Authors are already accountable.

Credit---If they really wanted credit attribution they would let us have AIs as authors. On the other hand, if an AI became an author then it will start complaining that its co-author isn't doing their share.

END BILL

Key Reasons for Disclosure

Human Accountability: Generative AI tools cannot be listed as authors. Human authors are completely responsible for the veracity, correctness, and integrity of all material—including guarding against "hallucinatory references" or incorrect proofs.

BEGIN BILL: Already true without disclosure. END BILL

Differentiating Credit and Workflow: Different uses of AI—ranging from basic grammar checks to finding proofs, checking logic, or generating core mathematical results—represent very different levels of human effort and intellectual contribution. Transparency allows the community to understand how a result was achieved.

BEGIN BILL: So the community wants to know whether a human did it--just out of curiosity? END BILL

Research Integrity and Trust: AI models can generate authoritative-sounding errors, biases, or uncredited third-party text. Mandatory disclosure helps maintain trust and allows reviewers to properly evaluate the provenance of the research.

BEGIN BILL: If a paper is AI-generated then human reviewers should be on the lookout for errors (whether or not they are authoritative-sounding), biases, and uncredited third-party text. But shouldn't a referee check those items anyway? If disclosure is supposed to change how the referee checks the paper, tell me how. That would be an actual reason for disclosure. I ask all of this non-rhetorically.

END BILL

(Note: Minor copy-editing, spelling, or clarity improvements made by authors to their own text typically do not require formal disclosure.)

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

20 minutes into the future everyone will be using AI for their research on some level.

In that case human reviewers will need to check for

authoritative-sounding errors, biases, or uncredited third-party text.

Maybe ChatGPT will detect for them.

The New STOC Rules for the AI Era

The 59th ACM Symposium on the Theory of Computing takes place in Atlanta next June, part of the Federated Computing Research Conference. I don't usually do announcement posts but we need to talk about the Call for Papers (deadline November 2) where

In light of rapid advances in generative AI and their impact on research and scientific communication, STOC 2027 is experimenting with several new policies intended to encourage high-quality submissions and promote clear and effective communication of research. 

Let's talk about these changes, which seem more designed to limit the deluge of AI generated papers.

STOC 2027 submissions will not be anonymous; all listed authors must be human and are responsible for the submission.

This reverses the move to removing authors' names that STOC made in 2023. I was never a fan of double blind reviewing and you need authors who can take responsibility for the submission.

Each author may appear on at most five submissions.

Understood but it might hurt some students who have an active advisor. 

Every paper must be submitted to arXiv before the STOC paper submission deadline. Authors must provide a public arXiv URL or proof of arXiv submission along with their submission PDF, which must be identical to the arXiv version.

In the past you could submit preliminary results and try to extend them before publication, since reviewers were expected not to build on unpublished work they were reviewing. This rule may cause some authors to hold back submissions or use AI to help with the extensions.

Authors must submit a video explaining the work, its context, and its innovations relative to prior work. The video should be 20–30 minutes long and will be due 1–2 weeks after the paper submission deadline. The recording should be presented by at least one listed author. The written submission remains the primary object of review. 

This rule will both check that at least one author understands the paper and add some friction to just generating papers using a few prompts. AI could generate the video of an author explaining the paper, but at least for now that would be prohibitively expensive. Some might use AI to generate the script but that would likely be easy to tell from the video. 

I worry that judging the paper based on the video will hurt those who aren't native speakers of English, and might exacerbate unconscious biases so I hope the reviewers really do focus on the paper for the actual review.

Authors may use large language models (LLMs) and other generative AI tools in preparing papers. Substantive use must be disclosed in the paper; minor copy-editing and grammar or clarity improvements to the authors’ own text do not require disclosure.

I would go further and make all papers have an AI disclosure, even if it is just minor copy-editing or "No AI was used in the production of this paper".

Program committee (PC) members and external reviewers (sub-reviewers) may use LLMs to assist with reviewing. Authors must explicitly consent as part of the submission process. All reviews and decisions remain the responsibility of the PC members and sub-reviewers.

I would require consent as condition of submission especially since AI models already have access to arXiv papers. Recent AI models have greatly improved their ability to check proofs if prompted correctly so the overworked PC members can focus on paper quality. 

---

We really need a larger conversation about the role of conferences in theoretical computer science if one can now generate papers from prompts. I've long argued that we should focus the conference more on connecting the community than the "journal that meets at a hotel". The STOC TheoryFest has helped but it would be great to get further away from lauding papers that have complicated proofs and focus more on the ideas that truly drive our field.

I don't care about majors, minors, or honors programs. Do you?

The following conversation is fictional.

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

ALICE: (Looking over a student's record.) Hmm, let's see. She wants to work in quantum computing. She's had the year-long quantum sequence in the physics department and has taken a course in quantum computing in the computer science department. She has done a project in quantum computing in an REU program.  Grades good, letters good. I think we should admit her.

BOB: Wait! Did she get a minor in Physics? This is very important!

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

When looking over a student's record the questions

Does she have a minor in X? or

Did she double major?  or

Did she graduate with honors? 

never dawn on me.

1) When I am on an admissions committee I look at:

a) Transcript: What did they take? The grades are generally good so that's a minor factor.

b) Letters that tell me what they did within STEM. I don't care about ballroom dancing or moral character. 

c) Papers they've written whether or not they have been published.

d) Their personal statement. They need to tell me:

i) Why they want to get a PhD.  When Ted Kennedy challenged Jimmy Carter for the presidential nomination in 1980, Ted Kennedy was asked Why do you want to be president? See here for his rambling and incoherent answer.

Despite his background in proving lower bounds on approximation contingent on the Unique Games Conjecture, Ted Kennedy would not have gotten into our graduate program.

ii) What they are interested in (this may have been covered in part (i)).

iii) Why they are qualified.

2) Do I care what the major is? No. I care that they know computer science which I can get off of their transcript.

3) Do I care if they double major in (say) Math. No. I can look at the transcript and see what math courses they took.  I don't care what (possibly arbitrary) rules their school has for double majoring.

4) Do I care if they minored in (say) physics? Not even a little. If they want to do quantum computing I care if they have taken courses in that area.  I don't care what (likely arbitrary) rules their school has for minors.  I took five courses in Philosophy as an undergraduate. Did I get a minor? I don't recall.  Two of them were in logic so I don't think I deserve a minor.

5) Are they in their school's CS honors program? Some other honor program? Are they on track to graduate with CS honors? Some other honors?  I don't care what (definitely arbitrary) rules their school has for honors programs.  If they are writing a paper, honors thesis or not, I will want to hear about it from their letter writer and from their personal statement. 

6) Do I care if they are in phi-beta-kappa? Sigma-Xi? Tau-Beta-Pi?  The last two I only know about since I googled  is there an analog of phi-beta-kappa geared toward STEM  for this post. You can probably guess that I don't care about any of those things. 

7) The point is that these formal criteria: major, minor, honors are not important when I am doing admissions.

a) Are they important to students?

I've heard that high school students who are honors students get a bumper sticker for their parents car that says:

                 My kid is an honors student at blah high school.

I would be more impressed if the bumper sticker said

                 My kid can prove the polynomial van der Waerden theorem.

b) Are they important to other people on the admissions committee?

8) Has the scenario I paint at the beginning of this post ever happened?

AI and Manufacturing Redux

ITMS 2026

Two years ago I attended the International Manufacturing Technology Show in Chicago's McCormick Place and found a rather limited focus on artificial intelligence among the exhibitors. ITMS is back in town so I went again this week. A quiet respite from all the AI/math angst, though that will come in full view when mathematicians take over the same venue in January.

I picked up my badge, the last to say "Illinois Tech" as I registered for a free academic pass well before the layoffs. Of course, you get to see all sorts of neat machines that make stuff but I tried to focus on where artificial intelligence plays a role. This time you could see AI everywhere, though as one exhibitor said, more of a marketing scheme than deep use of modern artificial intelligence. Real artificial intelligence did make appearances: vision recognition for robotic arms, backend software such as bid, invoice and document generation, predictive maintenance, and a variety of robotics, though mostly arms for assembling, cutting and even welding. 

I didn't see much of humanoid robots, digital twinning, use of large language models or manufacturing on demand. When do we get to the point that I can describe a product and have it designed, made and shipped to me quickly?

Not soon. I talked with someone from a small company that takes CAD designs and gets them ready for the manufacturing process. I asked him about automating the design phase and he said they leave that to ChatGPT. But OpenAI and Anthropic were nowhere to be found and Microsoft, Google and Amazon had scaled-down exhibits from two years ago.

Two years ago I remarked on the big booths for European and Asian manufacturers. This year had noticeably fewer giant foreign machinery stands. I'm guessing tariffs and trade uncertainty have dampened the influx of foreign suppliers.

China has gone all in on AI and manufacturing. I can imagine a Chinese slogan:

The US uses AI to make theorems, China uses AI to make products.

Math, AI, and the Navier-Stokes Equations

On September 1, 2026:

LANCE:  I'm surprised you haven't blogged about OpenAI solving 10 open math problems.

BILL: If I post every time an open math problem is solved by AI I won't ever post about anything else.

I'll wait until AI does something really impressive.

LANCE: How impressive does the theorem have to be?

BILL: I'll post about AI doing math once AI solves a Millennium Prize Problem.

LANCE: That might not be for a while.

BILL: Agreed.

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

On September 8, OpenAI announced it had solved the Millennium Prize Problem on the Navier-Stokes equations. 

On September 9, Lance blogged about the result, see here.

So here, at last, is my long-awaited post on math and AI.

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

In my May 24, 2026 blog post about the Erdős Unit Distance problem being resolved by OpenAI ,  see here. I suggested two possible futures:

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

ONE: While this AI-generated (or AI-assisted) result is impressive, it will be a rare occurrence. This result was actually a counterexample. The needed math was known. The result was interesting. This is a perfect storm that we might not see again for a while.

TWO: Even before the AI revolution, when I came up with a math problem I wanted solved, I would seek help, perhaps too early. My curiosity far exceeds my ego.  Since AI makes it easy to get help, my fear is that eventually we will all be Bill Gasarch---scary.

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

Option ONE did not age well.

1) Rare occurrence? In August 2026, OpenAI solved ten math problems; see here. 

2) Only counterexamples?  The distinction between proving a conjecture and finding a counterexample may be an illusion. Even the disproof of the Erdos Distance Conjecture had to find an infinite number of counterexamples, which is close to a for-all statement.

3) The needed math was known?  To say that AI will only solve problems where the needed math is known seems odd. I suspect 99% of all theorems use math that is already known.

4) The result was interesting? All ten math problems OpenAI solved do all seem interesting.  Or, more rigorously, there exists N large (maybe around 100) such that, for all P, where P is one of the ten problems, there exists at least N people who care about P.

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

Other Points

1) On Aug 12 Terry Tao posted here  about Sendov's conjecture: Let \(n\ge 2\) and let \(p \colon C \rightarrow C \) be a degree \(n\) polynomial with zeros in the unit disk. Then for every zero a of \(p\), there exists a critical point \(\zeta\) with \( |\zeta - a | \le 1\)

a) The conjecture for \(n\le 8\) was known.

b) Terry Tao had shown that the conjecture was true for large \(n\).  No lower bound on \(n\) was known.

c) Lech Mazur was able to use an AI tool to resolve the conjecture. See here

d) The post by Terry Tao was a digestion of the proof.

Digestion is just the right term. I nominate it for word of the year for 2026.

2) This may be the future: AI assists us but we still need to digest the proofs.

3) Will we bother with the digestion? Or will we be like students who use ChatGPT to do the homework and then do not read it carefully enough to learn anything from it?

Perhaps future papers will be in two parts: the proof, and the proof that the author actually read the proof.

4) Might we all become embodiments of the Chinese Room? We ask AI a math question, it supplies the proof, and we rewrite the proof without really understanding it.

5) I hope we will all be Terry Tao: digest the proofs and maintain understanding.

6) The four color theorem: the basic idea was human-understandable, but a program was needed to check an enormous number of cases (even in the later proof).  Question: Are there any results where all we have is that a program said it was true and we lack the basic idea? Of course, many proofs in math were done by humans, but I do not understand the basic idea.

That is, has this SMBC cartoon happened yet: see here  

7) Riemann: I quote Wikipedia (see here)

In August 2026, an unreleased research version of the Anthropic's large language model Claude working interactively with human researchers, proved unconditionally that at least two-thirds (66.6%) of the non-trivial zeros of the Riemann zeta function lie on the critical line.[44] Using an optimized test family, this bound has been improved to

\(\frac{3}{2} - \frac{1}{\sqrt{2}}\cot(\frac{1}{\sqrt{2}})\sim 67.25\%\).

Is this progress towards a solution?  Is RH going to be solved soon? 

8) The Navier-Stokes equation problem. Very roughly, the question asks if a certain class of equations always has a smooth solution. OpenAI has announced that they found a counterexample. There are some issues with this. Here is a quote from the Wikipedia entry on the NS equations (see here)

The announcement [by OpenAI] was accompanied by a priority dispute with Levent Alpoge (employed at a rival AI company Anthropic) and Tristan Buckmaster, who derived a set of closely related results on the Euler equations. The method used to generate the claimed solution built upon a method developed by Diego Corboda and Luis Martinez Zoroa in 2023 to prove blowup phenomena in related fluid equations.

(ChatGPT wanted me to say Is the result AI-assisted or AI-generated rather than assert that it is AI-assisted.)

9) Could Alpoge and Buckmaster have solved the problem?

(The name Alpoge looked familiar to me so I searched the blog to see if I had mentioned him before. I had! He was the first person to prove that the primes are infinite using Ramsey theory. See that post here.)

10) Will people be scared to use AI when they are beginning to work on a proof for fear that AI will scoop them?

11) OpenAI has said it will not try to collect the money. This is the SECOND Millennium Prize Problem where the solver turned down the money, though for different reasons. I do wonder what will happen the next time AI solves a problem worth money---who gets the money?  Perhaps the prize should go to whoever can explain the proof to the prize committee.

12) Shortly after the story broke Terry Tao had a blog post on it. He later had some guest posts about Math and AI. I was going to point to Terry Tao's posts and guest posts, but you can all use Google to find those posts, or ask ChatGPT to summarize them.

13) What about disclosing that you used AI for a paper?

Perhaps in the future 'written with AI assistance' will sound like written with a word processor.

My proofreader points out that predicting the future is stupid since most people can't even figure out what the present is.

14) PhD students in math will use AI (they probably already are).  AI will produce proofs that the students could not have found themselves.  Do they deserve a PhD if they can digest those proofs and rewrite them in an  understandable way?  I think the answer has to be YES: banning AI will be both impossible and undesirable.

Asking math PhD students to understand their own thesis might actually make getting a PhD harder.

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 the 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.