Theoretical computer science has a reputation as the quiet corner of the field. Its practitioners prove theorems about what can be computed, how fast, and with how much memory. There are no product launches and few benchmarks. So when AI started showing up in this world, it raised an obvious question: can a system that learns from data say anything useful about a discipline built on proof?
The honest answer is "yes, in a few specific ways, and no, in many others." Let's separate what's actually happening from what's mostly noise.
Two directions of influence
It helps to split the topic in two. First, AI as a tool that theorists use. Second, AI as a subject that theorists study. Both are growing, and they feel quite different.
AI as a tool: searching for things humans haven't found
The most concrete results come from using machine learning to search huge spaces that humans can't explore by hand.
A well-known example is DeepMind's AlphaTensor, announced in 2022. It treated matrix multiplication as a kind of game and searched for ways to multiply matrices using fewer basic operations. It found new algorithms for certain matrix sizes, and for some cases improved on what had stood for decades. The result wasn't a revolution in the theory of fast matrix multiplication, but it showed that a learned search could discover real, checkable improvements.
Later systems pushed the idea further. DeepMind's FunSearch paired a language model with an automatic evaluator to propose programs, then kept the best ones. It produced new constructions for a problem in extremal combinatorics known as the cap set problem. More recently, AlphaEvolve took a similar approach with evolving code and reported improvements on a number of problems, including a way to multiply certain small complex matrices with fewer scalar multiplications than previously known.
Notice the shared pattern. The AI doesn't "understand" the math in a human sense. It proposes candidates, and a separate program verifies them. That verification step is what makes the results trustworthy. A found construction either works or it doesn't, and anyone can check.
AI and formal proofs
Another thread is automated and assisted theorem proving. Proof assistants such as Lean let mathematicians write proofs in a language a computer can check line by line. That makes them an ideal partner for AI, because any proof the AI suggests can be verified mechanically. A wrong answer simply fails to compile.
Systems like DeepMind's AlphaProof reached a level comparable to a silver medal on International Mathematical Olympiad problems in 2024, working in Lean. Olympiad problems aren't research mathematics, but the result mattered because it combined learning with strict verification.
For theoretical computer science, the payoff is mostly practical for now. AI can help with routine lemmas, suggest proof steps, and fill in tedious case analysis. Researchers still decide what's worth proving and why. And a proof being formally correct doesn't tell you whether the question was interesting.
The caution: language models and proofs
It's tempting to ask a chatbot to prove a theorem, and sometimes it works well, especially for known results. But there's a real risk. Language models can write proofs that look polished and confident while hiding a gap or an outright error. In a field where one subtle mistake invalidates everything, that's dangerous.
The sensible workflow is to treat model output as a suggestion, not a result. Check it yourself, or better, check it with a formal verifier. Many working theorists describe using these tools for brainstorming, literature search, and checking intuition, while keeping the rigorous work firmly in human hands.
AI as a subject: what can these models even compute?
The second direction flips things around. Instead of using AI to do theory, theorists study AI with the tools of theory.
A central question is what a transformer, the architecture behind most modern language models, can and cannot compute. Researchers analyze this using circuit complexity and formal logic. Results in this area suggest that, under certain assumptions, a fixed-depth transformer without extra steps is limited to a fairly weak class of computations. Certain problems that need long chains of sequential reasoning are out of reach in a single pass.
This connects to a practical observation: letting a model "think out loud," producing intermediate steps before the answer, appears to increase what it can compute. Theoretical work has shown that chain-of-thought style generation can, in principle, expand a transformer's power considerably. That's a nice example of theory explaining something practitioners noticed empirically.
Other open questions in this area include:
- Why do large networks generalize well even when they have far more parameters than training examples? Classical learning theory struggles to explain this.
- How do we describe the optimization landscape of training? It's non-convex, yet simple methods like gradient descent work remarkably well.
- What are the real limits of learning from data, and how much does the structure of a problem matter?
Many of these remain unsettled. Progress is real but partial.
Learning-augmented algorithms
A smaller but fascinating area is often called "algorithms with predictions." The idea is to take a classic algorithm, for example for caching or scheduling, and give it access to a prediction from a machine-learning model. If the prediction is good, the algorithm performs better than the worst-case bound. If the prediction is bad, the algorithm still guarantees decent performance.
This is a very theory-flavored way to use ML. It doesn't ask you to trust the model. It asks what you can prove regardless of whether the model is right. It's a good illustration of how the two worlds can cooperate without either one taking over.
What AI has not done
Because the hype is loud, it's worth being direct about the limits.
AI has not resolved any of the famous open problems. P versus NP is still open. So are the major questions about circuit lower bounds and the true complexity of matrix multiplication.
AI has not replaced theorists. Choosing the right question, building a new framework, and recognizing why a result matters are still overwhelmingly human activities.
And most of the headline discoveries involve narrow, well-defined problems where success can be checked automatically. Open-ended conceptual breakthroughs are a different matter.
How the culture of the field is changing
Even without grand breakthroughs, daily practice is shifting. Researchers use language models to summarize papers, translate between notation styles, write quick scripts to test conjectures, and catch simple errors. Students use them to get unstuck on exercises. Formal verification is getting more attention because it pairs so naturally with AI.
There are real concerns too. If AI-generated proofs become common, how do journals verify them? How should credit be given when a system finds a construction? And how do we avoid a flood of low-quality, auto-generated papers that look rigorous but aren't?
These are questions about norms rather than technology, and the community is still figuring them out.
What to watch next
If you want to follow this area, a few developments are worth keeping an eye on. First, progress in formal proof systems, since verified results are the safest way to trust machine-generated mathematics. Second, theoretical work on what reasoning models can do and what they fundamentally can't. Third, new search-based systems that propose and test algorithms, because that's where the clearest real wins have come from so far.
The short version
AI is changing theoretical computer science in two ways. It's becoming a search and assistance tool that can uncover constructions humans missed, as long as results can be verified. And it's becoming an object of study, forcing theorists to ask hard questions about learning, generalization and computation.
It isn't replacing the discipline. If anything, it's making the core theoretical habits more valuable: precision, proof, and a healthy suspicion of anything that sounds convincing but hasn't been checked.