Blog

LLMs for Proof Generation and Verification

Guanyang Wang中文

In June 2026, I used ChatGPT 5.5 Pro to obtain a proof of the Kannan–Tetali–Vempala (KTV) conjecture. My collaborators, Weibo Fu and Qian Qin, and I then checked it carefully. Afterward, I used Codex to formalize the proof in Lean.

The theorem matters in its own right. Posed in 1997, the KTV conjecture asks whether the swap chain mixes rapidly for every feasible choice of row and column sums. At its core is a basic sampling problem: drawing a uniformly random binary matrix with prescribed margins, or equivalently a uniformly random bipartite graph with prescribed degrees. The swap chain is a standard sampler for fixed-margin null models in ecology, statistics, and network analysis. Our theorem resolves the binary-matrix case after nearly three decades: it gives a worst-case optimal spectral-gap bound for every feasible set of margins, a result stronger than the original rapid-mixing conjecture itself.

Yet what stunned me even more was how the result was obtained and checked. In both proof generation and formalization, LLMs performed far beyond what I had expected.

I have little doubt that this will change how mathematicians work. I think our experience points toward a workflow that may become common: an LLM generates a proof; humans inspect it, steer the process, and take responsibility for the result; an LLM turns the proof into Lean; and Lean’s kernel checks the formalization. As LLM-generated proofs proliferate, verification may become a bottleneck. Pairing generation with machine-checked formalization offers a plausible way for mathematical discovery and trustworthy verification to scale together.

That is why I decided to document how we obtained and checked this proof. I wanted to leave a concrete record of how the workflow played out in practice, in the hope that it will be useful to others.

The proof itself took only a handful of prompting rounds. The Lean formalization took Codex about 100 hours, consumed an entire week of my Pro quota, and initially produced roughly 100,000 lines of code.

This post is not about the mathematics of the proof itself. Readers interested in that should see our paper and the forthcoming slides.

Other Recent Cases

Since completing our project, I have learned about several related efforts by other researchers. I am collecting them here for reference:

How the Proof Was Found

My prompting strategy was almost embarrassingly simple: I gave the model the problem and asked it to prove or refute it. Some of the prompting in the examples above may be considerably more sophisticated.

There was, however, one intervention worth describing.

GPT-5.5 Pro first identified the mainstream approach to the problem—P-stability—and tried to push that line of attack forward. It did not succeed. I knew enough about the method to suspect that P-stability alone was unlikely to resolve the general case, so partway through the process I told the model not to remain attached to the existing approach and to look instead for something more algebraic.

That change of direction altered everything. From that point on, GPT worked almost autonomously and produced the proof within a few more prompting rounds.

To be clear, when I suggested an algebraic approach, I did not know that it would work. If I had known, I might have solved the problem myself. I simply saw that the model was stuck and nudged it toward a different road.

The human-in-the-loop contribution in this case was therefore mostly one high-level directional prompt. What I find striking is that such guidance can be effective even when the human does not know where the new direction will lead.

Now that GPT-5.6 is available, a more natural workflow may be to use Sol inside Codex rather than work through the browser as I did. Codex’s /goal command may be especially useful: it can keep GPT working on a problem for dozens of hours.

From the Proof to Lean

After my collaborators and I had checked the proof by hand, I tried asking Codex to formalize it. At that point, I had never written Lean. I did not even have Lean installed on my computer.

Codex had already been enormously useful in my other projects, but asking it to write Lean began as an experiment that I did not expect to go very far.

I started by setting a /goal and asking it to formalize only a small part of the argument. Its performance in each round was far better than I anticipated, so I gradually expanded the target until I was asking it to formalize the entire paper.

The process was not completely smooth. Codex sometimes got stuck when it encountered mathematically standard facts whose details had been omitted from the paper. Its characteristic failure mode was not an obvious error. Instead, it would repeatedly prove closely related or redundant lemmas without making real progress on the main proof.

When this happened, I brought in Claude Code, using Sonnet or Opus, to audit the code. In places where I could judge the mathematics directly, I also asked GPT to write a more detailed natural-language proof first and then passed that proof to Codex. In the end, we resolved all of these issues.

Once the formalization was complete, I asked Codex to carry out a thorough refactor. This reduced the codebase from roughly 100,000 lines to somewhere between 70,000 and 80,000 lines. I also ran several additional rounds of auditing to confirm that the formalized statement genuinely matched the main theorem in the paper.

My estimate is that the entire process was about 95% automated. My main role was to keep Codex from becoming trapped in loops of equivalent or repetitive arguments.

There is a slightly embarrassing coda: by the end of the project, I still could not write Lean myself—although I had at least learned to read a little of it.

FAQ

1. Why formalize the proof in Lean?

Reviewing an LLM-generated proof is fascinating, but it is also nerve-racking. A proof handed to you by a model does not feel quite like one you developed line by line yourself. Even after several rounds of checking, I sometimes worried that we might have missed a detail.

Over a longer time horizon, LLMs will undoubtedly prove more theorems, including more important ones. But it will be difficult to eliminate the concern that any particular proof may contain a hidden error. As early practitioners of what one might call vibe mathing, I think we have a responsibility to give our colleagues a proof they can trust.

Lean is not the only way to verify a proof, and its libraries are still immature in many areas of mathematics. But it is an excellent option. It allows us to redirect some of our attention from “Is this proof actually correct?” toward understanding the mathematics itself.

2. What kinds of conjectures can LLMs solve?

I suspect: quite a lot.

My current guess is that LLMs can already handle problems of roughly the following kind:

Nearly all the ingredients already exist, but no one has yet seen how to assemble them into a complete global proof.

I do not think current models can solve problems that require building an entirely new theoretical framework from scratch. But they can carry out complicated calculations, produce clever ideas, and combine techniques from different areas.

Which problems in your own field sit at that level?

3. How many attempts did this take?

This was the first mathematical conjecture I tried to solve through prompting.

I only subscribed to Pro in May. I had mainly been using Codex for research related to diffusion models. In fact, I have gradually moved away from theory over the past few years, so this is definitely not a story in which I tried hundreds of problems and reported the one success.

After solving this problem, I did try several others. Some were not public conjectures, but simply questions that interested me. The results were mixed.

4. What might this mean for mathematics?

In the short term, I think we are entering a “prompt era.” We will see many new advances and many new proofs, and verification may become the bottleneck that follows.

The good news is obvious: important new results will be discovered. The less comfortable consequence is that LLMs may sharply compress the value of solid but non-landmark results. The same dynamic may apply to other theoretical fields, including learning theory, theoretical statistics, econometrics, and theoretical physics.

5. What might this mean for mathematicians?

I do not know.

For someone like me—with a mathematical background, but gradually moving into other areas—the experience has been almost perfect. It gives me an excuse to return, in spare moments, to questions that once fascinated me but that I could not solve.

For people whose careers are entirely in mathematics, the experience may be much more complicated. A problem that someone has worked on for years might be solved by a model in a very short time.

There is also a more constructive possibility. LLMs may let problem solvers tackle much harder problems, while theory builders may collaborate with models in a different way: using mathematical taste and high-level judgment to guide the construction of new theories.

6. What are the main takeaways?

Three conclusions stand out to me.

First, LLMs are already extraordinarily capable. I have no doubt that they will change how people do mathematics.

Second, Lean verification was far easier than I expected: with an LLM, you do not even need to know Lean to produce a machine-checked formalization. The code is far below mathlib standards, but can be enough to check that a theorem is merely true. This example may be biased, however, because Lean support remains incomplete in many fields.

Third, my advice is simple: test boldly and verify rigorously. There is a Chinese saying, often quoted sarcastically, 人有多大胆，地有多大产—roughly, “the bolder you are, the greater the harvest.” With current models, it may be unexpectedly apt. Ask them to attempt problems you would not previously have dared to try. Each attempt is also a probe: watch what the model can do, where it fails, and where human taste and judgment remain indispensable. That is how we map the boundaries of these systems.

I’m off to diffusion models. Happy prompting! If a model surprises you, consider buying me a coffee. ☕