I Spent a Year Asking AI to Solve Math’s Hardest Problem. Here’s What Happened
It started almost by accident. At my startup Dwelly, I constantly push the limits of what AI tools can actually do. One day I just typed into a chat: “Can you prove P ≠ NP?”—referring to the problem the math community has been stuck on for decades.
The model basically laughed at me. But the question stuck. It felt like the perfect stress test for modern AI. I was convinced this was only a matter of time, that advancing technology would eventually make problems like this meaningfully more tractable. And if a system could crack something like this, it could probably handle autonomous SMS service development, too; which, back in early 2024, was still an open question.
I have a bachelor’s in applied math and a master’s in applied computer science with an AI focus, but I wouldn’t call myself a professional mathematician. My role is closer to prompt engineer: I guide the models, verify their reasoning, do research, and assemble fragments into a coherent proof. I like to think of myself as conducting an orchestra: different LLMs, engineering agents, research agents, auditing agents, all working together toward the same goal. Like a conductor, I watch the score constantly, making sure nobody’s playing off-key or flattering me instead of doing the hard work.
I won’t claim I’ve cracked it, but after a year of attempting this with LLMs, and eight months of intensive work since agentic tools like ChatGPT Codex appeared (roughly 8,000 queries across different models), I’ve developed real confidence in my process. I’ve built a unique, verifiable pipeline for attacking this problem, one that systematically tests hypotheses and closes gaps.
I now have a formalized proof skeleton. I’ve analyzed all the major publications. I’ve identified the key gaps (currently still assumptions) and I’m methodically closing them. No, I can’t claim an unconditional result yet; only a complete proof would qualify. What I do have is an internal sense, from watching my AI orchestra tackle problem after problem, that we’re moving forward in a real direction.
What is P ≠ NP, and Why Does It Matter?
Think of a computer as a machine that solves problems. Some problems it solves quickly, in time that grows polynomially with input size. That’s class P. Sorting a list, finding the shortest path in a graph.
Other problems are easy to verify once you have an answer, but finding that answer yourself can be brutally hard. That’s class NP. Classic example: the traveling salesman problem. Given a list of cities and distances between them, checking whether a proposed route is good takes linear time. But finding the optimal route among all possible combinations is exponentially hard.
P vs. NP asks: are these two classes actually the same? If P = NP, then every “hard” problem is secretly fast to solve; we just haven’t found the right algorithms yet. That would upend cryptography, optimization, logistics, and AI. Most experts believe P ≠ NP, but no one has proven it. The Clay Mathematics Institute has a $1-million prize waiting.
How I Approached It
The problem space is enormous. To prove P ≠ NP, you just need to take one specific NP-complete problem—say, 3-SAT—and rigorously show it can’t be solved in polynomial time. The catch: there are infinitely many such problems from which to choose. Picking the right one is like trying to find a rock on the side of the road that fits perfectly in your hand; they all look fine at first glance. Different researchers grab different problems; some approaches overlap, most don’t.
My first move was having models collect and cross-reference all existing results, bringing the full mathematical context into one place. Within a few months, we ran into what are called barriers: fundamental limitations that cut down almost every known proof attempt.
There are three main ones:
Relativization: Many proofs still “work” even when you add an oracle (a black box) to the computation. However, P and NP behave differently in different oracle worlds, so techniques that relativize can’t separate the classes in the real world.
Natural proofs: Arguments that rely on “natural” combinatorial properties are actually too powerful; they’d break pseudorandom generators, which we believe is impossible.
Algebrization: Even algebraic techniques, like arithmetization, fail in the same way; they collapse under certain oracle constructions.
Any real proof has to navigate around all three simultaneously. Most attempts drown at the first one.
The Bridge Metaphor
Building such a proof is like trying to construct a bridge across a river of unknown width. You pick a starting point on one bank and a target on the other. You drive in pilings, lay planks, inch forward. At any point you can jump to a different spot and start building from there instead.
First problem: you don’t know how wide the river is. You might keep needing more and more material without any way to know when you’ll reach the other side.
Second problem, far worse: the river has pits of incomprehensible depth; the barriers. They don’t just swallow your material; they pull down everything you’ve built. You have to start over: pick a new path, find a new starting point, build an entirely different bridge.
How I Actually Work
As the conductor of this AI orchestra, my main tools are skepticism, persistence, the ability to hold the full project context in my head, and knowing how to specify exactly what output I need at each step.
Early on, I pushed the models to be creative: generate dozens of candidate “hooks,” specific NP-complete problems or approaches that might navigate around the known barriers. When one looked promising, I shifted into deep research mode.
What became clear over the course of this work is that access to the most capable model, and the routine effort of tracking model updates, is not, in fact, the hardest problem. The harder problem is understanding which model resolves which class of task most reliably, and then actively managing who does what, in what order, under what constraints. That orchestration layer, the decisions about routing, critique, authority, and verification, is where the real engineering lives.
Everything happens in Lean 4, a language for formally verifying mathematical proofs. A theorem in Lean compiles like code. If it does not compile, the proof contains an error. Every output I receive from any language model gets translated into Lean, and the compiler automatically filters out the nonsense. This single constraint dramatically raises the reliability of the entire search.
To make that search productive, I run four models simultaneously. They are, in principle, interchangeable; any one of them can attempt any task. But on problems of this complexity, the goal is maximization: squeezing the absolute most out of every tool available. And that maximum is only reachable when each model is deployed against the class of problem it handles best.
ChatGPT 5.5 Pro serves as the system’s primary reasoning engine: the designated brain, the one ultimately responsible for forward progress and for ratifying any final decision.
Gemini 3.1 Pro handles the discovery layer: finding unexpected conceptual bridges between distant bodies of literature and surfacing existing research that would otherwise take months to locate manually. Its Deep Research mode is, in practical terms, a replacement for a significant portion of traditional literature search.
Independent agents running on OpenAI Codex write the Lean code itself, perform automated testing, handle optimization passes, and re-verify proofs under perturbation. A separate instance running Leanstral is tasked specifically with hunting for unexpected bugs and silent logical failures, the kind of error that looks locally valid but breaks the global structure.
Orchestrating all of this is Claude Code, acting as chief engineer: it manages the more specialized models, monitors their outputs, and maintains coherent state across the pipeline, while itself remaining accountable to the reasoning engine above it.
The models are deliberately pitted against one another. One model’s output is fed to another for adversarial critique; the feedback is routed back. I adopt the role of an expert mathematician in these exchanges, because the models respond with noticeably more precision when they treat the interlocutor as a peer capable of catching errors. Without that framing, the self-criticism is too weak to be useful: a single model left to evaluate its own output can write the axiom 2 = 1, derive conclusions from it, and fail entirely to notice.
Where I Am Now
I have a complete formalization of the P ≠ NP problem. All major publications have been analyzed and translated into code. I have an overall proof structure and a small number of clearly identified gaps: assumptions under which the problem is already solved. My current focus is turning those assumptions into proven statements.
I believe I’m the first to approach this problem this specific way: human + specialized LLM orchestra + formal verification in Lean.
If you are interested in diving deeper into my research, here you can find a link to my repository: https://github.com/khanukov/p-np2
The Bottom Line
Individual LLMs still lack genuine self-criticism and real creativity. But when a human conducts several models well—cycling feedback between them, making them challenge each other—something larger emerges; effectively a super-AI, capable of attacking millennium-level problems.
My experiment suggests that the limits of what we can do with LLMs in fundamental science are expanding much faster than most people think. The next breakthrough in complexity theory might not come from an elite academic office; it might come from a chat window where a human and a set of machines are together building a bridge across a river humanity hasn’t crossed in decades. If it works, it means we’re seriously underestimating AI even now, at the height of the hype.
Dmitry Khanukov is a seasoned entrepreneur and technology leader with over two decades of experience in building and scaling B2B tech products, AI platforms, and B2C marketplaces. As co-founder and CTO of Dwelly, an AI-enabled letting and property management marketplace, he applies deep expertise in strategic leadership and product development.
Submit an Article to CACM
CACM welcomes unsolicited submissions on topics of relevance and value to the computing community.
You Just Read
#### I Spent a Year Asking AI to Solve Math’s Hardest Problem. Here’s What Happened
© 2026 Copyright held by the owner/author(s).
Join the Discussion (1)
#### Become a Member or Sign In to Post a Comment
1. “Like a conductor, I watch the score constantly, making sure nobody’s playing off-key or flattering me instead of doing the hard work.” Such an approach is for the few and may wear out in the future. From now on, in the age of AI, we should all take addiction into account. Most of us, starting with scientists, put AI above all else, because they see positive results and now they have started to forget how they worked before! With businesses, things become complicated at the altar of competition. However, one of the most significant risks concerns the Next Generation, our students: <https://www.linkedin.com/posts/panagiotis-gioannis-3b8605186%5Fstudents-could-soon-get-degrees-without-share-7464345439908081665-Iw8f/> \[Students ‘could soon get degrees without reading a book’\] Please take a look at the internal links, as they contain important examples. also, <https://www.linkedin.com/posts/panagiotis-gioannis-3b8605186%5Fit-is-incredible-how-ai-is-transforming-share-7462744116578164736-mZPQ> \[‘It is incredible’: How AI is transforming mathematics\]
News Jul 21 2026
How to Cross the AI Code Productivity Divide
Artificial Intelligence and Machine Learning
BLOG@CACM Jul 20 2026
If You Think You Can Do Real-World Text-to-SQL
Michael Stonebraker and Peter Baile Chen
Artificial Intelligence and Machine Learning
News Jul 20 2026
Dame Wendy Hall Receives Sir Frank Whittle Medal
Shape the Future of Computing
ACM encourages its members to take a direct hand in shaping the future of the association. There are more ways than ever to get involved.
Communications of the ACM (CACM) is now a fully Open Access publication.
By opening CACM to the world, we hope to increase engagement among the broader computer science community and encourage non-members to discover the rich resources ACM has to offer.