> What I’ve found is that given a tool that can detect mistakes, the agent can often correct them
This is the most important line of the entire article
When iterating on a Manifesto for AI Software Development (https://metamagic.substack.com/p/manifesto-for-ai-software-d...) over the last two years the key attribute more than any other that I found was empirical validation. While AI (and humans) are not able to accurately judge their own work when we give AI (and human) the ability to do empirical validation its success skyrockets. This might be intuitive, but there are still papers testing that this applies to AI too. While reaching to have the AI write unit tests I've been embracing fuzzing because then AI can't cheat with bonus tests. The idea of reaching back to school and using interactive theorem proving didn't even cross my mind and now that it has been presented it is a whole paradigm shift on how to push my AI use forward so it can work even more autonomously.
AI can iterate at speeds humans can't. When it has even basic empirical validation (building the code, running tests) it removes the human from the loop. Move that to using fuzzing (such as with golang) and you get way better coverage and way better progress before a human has to intervene. So it isn't a surprise that interactive theorem proving is a perfect match for AI.
It is interesting how this same lesson plays out elsewhere, earlier in the article
> Why is ITP so hard? Some reasons are quite obvious: interfaces are confusing, libraries are sparse, documentation is poor, error messages are mysterious. But these aren’t interesting problems
Remember when llvm got really good c++ error messages and it was life changing? High quality error messages means we could find/fix the error fast and iterate fast. These are actually the MOST interesting problems because it enable the user to learn faster. When a user has high success they will use a product again and again. High quality error messages in all tools will enable Claude code to be able to work longer on problems without human intervention, make less mistakes and overall work faster.
While error messages should always be good a new question that really hammers this home is "When AI encounters this error message, can it fix the problem?"
Combining generative ML (and other heuristic methods) with formal methods is the most promising way forward for systems design. Without formal methods (and other constraints such as limiting systems complexity) we are going to vibe-code ourselves to chaos.
I think everyone who has heard of interactive theorem provers saw that this is going to be a match made in heaven.
LLMs reduce implementation effort but pile on massive review effort. Interactive theorem provers reduce review effort but the implementation is much more work.
Together you get the best of both worlds at the speed of machine thought.
I will quote (approximately) Simon Peyton Jones: "writing programs is not hard. Specifying what a program should do is hard."
Prove what? The author is well versed in the problem of specifications as the aliens-demand-gcc-correctness-or-else post. I also enjoyed the other post where they say "no one cares about correctness" and "people care about compliance".
It is safe to say, most people are not experts and will never become experts.
Being proficient in the business of coming up with suitable specification that can be implemented and getting assurance that an implementation meets the spec will most likely need all the kind of formal training for humans that the AI hype industry assures us is no longer necessary.
So it doesn't much help that LLMs are good at manipulating the tokens when used by experts, at least not in a big way. It can be hoped that they change cost-benefit balance in good ways, but the bigger problems of the industry will simply persist.
What would need to change for a more fundamental shift is getting a lot more people to understand the value of specifications. This is an education problem and paradoxically I could see AI helping a lot... if only there was enough interest in using AI to help humans become experts.
Among other general advice, my CLAUDE.md insists Claude prove to me each unit of change works as expected, and I'm usually just hoping for it to write tests and convince me they're actually running and passing. A proof assistant seems overkill here, and yet Claude often struggles to assemble these informal proofs. I can see the benefit of a more formal proof language, along with adding a source of programmatic feedback, compared to open-ended verbal proof.
"Overkill" of course is an editorial word, and if you know about https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... then you know many statically typed programming languages are essentially proof assistants, where the proof goal is producing well-typed programs. LLMs are already quite good at interacting with these programming language proof assistants, as you can see any time a competent LLM interacts with the Rust borrow checker, for example.
I’ve been working with gpt-5-high recently and while it’s slow as molassess it’s also pretty darn impressive in what kinds of problems it can solve. I’ve given it coding tasks which Claude fumbled and it dealt with them given the same set of tools. It was honestly impressive; it feels like it’s on the verge of unlocking a new capability by being reliable enough.
I wouldn’t be surprised if the author was taken off guard by gpt-5 if he was already impressed by Claude code.
I've worked with Claude Code/Codex, and they're amazing, but I have a question.
I have never worked with tools such as Lean, but if an LLM writes a proof with Lean, how can one be sure that the code itself (in the proof) is correct? Or is Lean so strict that this is unlikely to happen?
I'm not at all surprised that LLMs are good at interactive theorem proving.
But I am surprised that Claude Code is good at it. Maybe I'm just not using it right but when I have a task in a less popular programming language, Gemini 2.5 pro tends to be much better than Claude Opus despite Opus doing better on benchmarks. Better in the sense that Gemini will typically bang out a correct solution with best practices immediately and Opus might take half a day of correcting basic errors and misunderstandings.
If anyone knows what I'm talking about and knows a way to improve this please let me know. Claude still feels to me like an over-eager engineer that is more eager to get thing done fast than to do them correctly. It may be that with a task like theorem proving you can just burn credits and time because there's a clear answer.
Buried about 2/3rds of the way through the article: “I’m about 50% of the way through the formalization plan…”
As soon as I saw this, I became a skeptic. Anyone who has used AI tools has seen cases where the first 80% of a project came together like a bolt of lightning, but the last 20% is next to impossible for the AI to accomplish, even if it doesn’t seem more complex than the rest of the code. AI just struggles as the code gets larger and the requests get more specific. Anyway, never trust a programmer to accurately judge the “50%” mark. Once they are at 90%, they will need another 90% to cross the finish line.
My experience points to that until the last sorry is eliminated the math might look like it will fit together, but yet not ultimately all fit together.
My issue with formal proofs for code is that it assumes that the code is static and requirements are fixed and won't change. This assumption doesn't hold up in the vast majority of projects.
Surely LLMs can make this more practical but I think many projects suffer from a more mundane problem that they aren't architected properly. Without proper separation of concerns and proper abstraction, you won't get stability in the base modules, which means that you will have to re-evaluate and re-write tests and formal proofs constantly.
This neatly sums up my experience with Claude Code. It’s a brilliant tool - but one that often requires a tight leash. The challenge is that you won’t know when or where until you’ve used it extensively for your specific use case.
In the author’s case, producing a formal proof that inspires little confidence feels counterproductive. It’s very likely that we’re missing a key piece here: perhaps what’s needed is a model trained specifically to keep large language models on task, verify their output, and challenge them on our behalf.
That said, deep domain knowledge remains essential. Without it, things can easily get built in odd or unintended ways.
A practical workaround (for typical app development/not formal verification) may be to treat the system as a black box - relying on carefully written specifications or test cases. In many situations, that approach could be more effective than trying to wrestle certainty out of inherently uncertain processes.
> I find this very surprising, and you probably should too.
Why? My first assumption would be that Claude Code would be exceptionally good at writing Lean proofs, for many of the reasons given in the article. It's been on my todo list for a while to try out some of my coding workflows on proof writing. I'm glad OP did.
But why does he find this surprising? That wasn't laid out.
EDIT: To be clear, I'm talking about this bit:
> I think this is part of why Claude Code is surprisingly good at theorem proving. Lean is very strict in the programs it will accept. This makes writing Lean arduous for humans, but it means an AI agent gets detailed feedback.
I first encountered this in writing Rust programs, first with Cursor (using anthropic models), and now with Claude Code. Things have gotten better, but initially Rust was not very well represented in the training sets used, and the agents would be horrendous beginner mistakes. Writing Javascript-like code with Rust-ish syntax, and expecting it to work.
But the rustc compiler gives very good errors, with context and suggestions for fixing. In two or three iterations it would fix all the mistakes, without any need for me to get involved. And because Rust's type system and safety guarantees are so strict, by the time it gets it to compile it _probably_ works.
It's been my assumption since that experience (my first experience using a coding agent), that it would be very good at writing machine-checked proofs.
This matches my experience with Claude on other projects. Its output is much better when it can work against detailed specifications and tests, and Lean seems to be an extreme case of that.
17 comments
[ 0.24 ms ] story [ 37.3 ms ] threadThis is the most important line of the entire article
When iterating on a Manifesto for AI Software Development (https://metamagic.substack.com/p/manifesto-for-ai-software-d...) over the last two years the key attribute more than any other that I found was empirical validation. While AI (and humans) are not able to accurately judge their own work when we give AI (and human) the ability to do empirical validation its success skyrockets. This might be intuitive, but there are still papers testing that this applies to AI too. While reaching to have the AI write unit tests I've been embracing fuzzing because then AI can't cheat with bonus tests. The idea of reaching back to school and using interactive theorem proving didn't even cross my mind and now that it has been presented it is a whole paradigm shift on how to push my AI use forward so it can work even more autonomously.
AI can iterate at speeds humans can't. When it has even basic empirical validation (building the code, running tests) it removes the human from the loop. Move that to using fuzzing (such as with golang) and you get way better coverage and way better progress before a human has to intervene. So it isn't a surprise that interactive theorem proving is a perfect match for AI.
It is interesting how this same lesson plays out elsewhere, earlier in the article
> Why is ITP so hard? Some reasons are quite obvious: interfaces are confusing, libraries are sparse, documentation is poor, error messages are mysterious. But these aren’t interesting problems
Remember when llvm got really good c++ error messages and it was life changing? High quality error messages means we could find/fix the error fast and iterate fast. These are actually the MOST interesting problems because it enable the user to learn faster. When a user has high success they will use a product again and again. High quality error messages in all tools will enable Claude code to be able to work longer on problems without human intervention, make less mistakes and overall work faster.
While error messages should always be good a new question that really hammers this home is "When AI encounters this error message, can it fix the problem?"
LLMs reduce implementation effort but pile on massive review effort. Interactive theorem provers reduce review effort but the implementation is much more work.
Together you get the best of both worlds at the speed of machine thought.
Prove what? The author is well versed in the problem of specifications as the aliens-demand-gcc-correctness-or-else post. I also enjoyed the other post where they say "no one cares about correctness" and "people care about compliance".
It is safe to say, most people are not experts and will never become experts.
Being proficient in the business of coming up with suitable specification that can be implemented and getting assurance that an implementation meets the spec will most likely need all the kind of formal training for humans that the AI hype industry assures us is no longer necessary.
So it doesn't much help that LLMs are good at manipulating the tokens when used by experts, at least not in a big way. It can be hoped that they change cost-benefit balance in good ways, but the bigger problems of the industry will simply persist.
What would need to change for a more fundamental shift is getting a lot more people to understand the value of specifications. This is an education problem and paradoxically I could see AI helping a lot... if only there was enough interest in using AI to help humans become experts.
"Overkill" of course is an editorial word, and if you know about https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... then you know many statically typed programming languages are essentially proof assistants, where the proof goal is producing well-typed programs. LLMs are already quite good at interacting with these programming language proof assistants, as you can see any time a competent LLM interacts with the Rust borrow checker, for example.
I wouldn’t be surprised if the author was taken off guard by gpt-5 if he was already impressed by Claude code.
I have never worked with tools such as Lean, but if an LLM writes a proof with Lean, how can one be sure that the code itself (in the proof) is correct? Or is Lean so strict that this is unlikely to happen?
But I am surprised that Claude Code is good at it. Maybe I'm just not using it right but when I have a task in a less popular programming language, Gemini 2.5 pro tends to be much better than Claude Opus despite Opus doing better on benchmarks. Better in the sense that Gemini will typically bang out a correct solution with best practices immediately and Opus might take half a day of correcting basic errors and misunderstandings.
If anyone knows what I'm talking about and knows a way to improve this please let me know. Claude still feels to me like an over-eager engineer that is more eager to get thing done fast than to do them correctly. It may be that with a task like theorem proving you can just burn credits and time because there's a clear answer.
As soon as I saw this, I became a skeptic. Anyone who has used AI tools has seen cases where the first 80% of a project came together like a bolt of lightning, but the last 20% is next to impossible for the AI to accomplish, even if it doesn’t seem more complex than the rest of the code. AI just struggles as the code gets larger and the requests get more specific. Anyway, never trust a programmer to accurately judge the “50%” mark. Once they are at 90%, they will need another 90% to cross the finish line.
(I'm talking about regular programs, not other LLMs or GANs)
Surely LLMs can make this more practical but I think many projects suffer from a more mundane problem that they aren't architected properly. Without proper separation of concerns and proper abstraction, you won't get stability in the base modules, which means that you will have to re-evaluate and re-write tests and formal proofs constantly.
In the author’s case, producing a formal proof that inspires little confidence feels counterproductive. It’s very likely that we’re missing a key piece here: perhaps what’s needed is a model trained specifically to keep large language models on task, verify their output, and challenge them on our behalf.
That said, deep domain knowledge remains essential. Without it, things can easily get built in odd or unintended ways.
A practical workaround (for typical app development/not formal verification) may be to treat the system as a black box - relying on carefully written specifications or test cases. In many situations, that approach could be more effective than trying to wrestle certainty out of inherently uncertain processes.
Why? My first assumption would be that Claude Code would be exceptionally good at writing Lean proofs, for many of the reasons given in the article. It's been on my todo list for a while to try out some of my coding workflows on proof writing. I'm glad OP did.
But why does he find this surprising? That wasn't laid out.
EDIT: To be clear, I'm talking about this bit:
> I think this is part of why Claude Code is surprisingly good at theorem proving. Lean is very strict in the programs it will accept. This makes writing Lean arduous for humans, but it means an AI agent gets detailed feedback.
I first encountered this in writing Rust programs, first with Cursor (using anthropic models), and now with Claude Code. Things have gotten better, but initially Rust was not very well represented in the training sets used, and the agents would be horrendous beginner mistakes. Writing Javascript-like code with Rust-ish syntax, and expecting it to work.
But the rustc compiler gives very good errors, with context and suggestions for fixing. In two or three iterations it would fix all the mistakes, without any need for me to get involved. And because Rust's type system and safety guarantees are so strict, by the time it gets it to compile it _probably_ works.
It's been my assumption since that experience (my first experience using a coding agent), that it would be very good at writing machine-checked proofs.