11 ms·

Claude can sometimes prove it

219 points by lairv 1y ago

deleted 1y ago
[deleted]
r0ze-at-hn 1y ago
> 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-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?"
- cube2222 1y ago
  This. It’s actually extremely good bang for buck now to invest more time in various linters or static checking that enforce more correctness / project-specific rules. Not only does the AI help you write the linter in 10% of a time - linters are usually fairly short scripts that are easy to test in practice, so the happy path for AI). But asking the AI “make this linter pass” after you’ve e.g. done some extensive refactors, is very effective and time-saving.
lambdaone 1y ago
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.
- qayxc 1y ago
  > we are going to vibe-code ourselves to chaos. To be fair, we've been doing that even without AI for the past 5 decades.
ngruhn 1y ago
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.
burakemir 1y ago
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.
- AfterHIA 1y ago
  You read like Alan Kay's Quora and for that I salute you comrade.
- baq 1y ago
  This change is happening as we speak. My work repo is now sprouting with markdowns primarily intended for agentic consumption, but it’s all dense jargon communicating requirements and important design decisions in a way which is useful to me as a software engineer. The toil of writing these specs from low level code is much lower today, because LLMs also help with that immensely.
  - burakemir 1y ago
    There is a place for informal, prose specs, and I can easily agree that more people are nowadays describing their programs in English. The context here is formal specs though - adequately and precisely capturing the intended meaning (semantics) in a way that lends itself to formal verification. Interactive theorem proving is interactive because proof search is intractable; a human articulates the property they want to prove and then performs the "search". Apart from the difficulties of getting to that proof, it can also happen that all goes through and you realize that the property is not exactly what you wanted.
bnjmn 1y ago
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_correspondence 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.
baq 1y ago
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.
Tiberium 1y ago
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?
- enricozb 1y ago
  If it compiles, it typechecks. If it typechecks, the proof is correct. This is a consequence of the Curry-Howard correspondence [0]. From a pure mathematician's standpoint, the content of a proof is kind of (waving big hands here) irrelevant. It's more that the existence of a proof implies the theorem is true, and thus can be used to prove other theorems. Because of this "proof-irrelevance", a great foil to an LLM's propensity to hallucinate is something like Lean. In Lean, and in theorem provers oriented towards classical mathematics, the statement of the theorem being proved is what matters most. And due to Curry-Howard, the statement is equivalent to the signature/declaration of the function, which is what the human ought to verify, while Lean will verify the body. [0]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon....
  - omnicognate 1y ago
    If it compiles it definitely proves something, which may or may not be what Claude tells you it proves.
  - wild_egg 1y ago
    The thing I'm stuck on is that, yes, the proof is correct. But what guarantees do I have that the proof or theorem is actually representative of the program I'm trying to specify? And beyond that, what guarantees are there that the resulting end program actually adheres to either the specs or what has been proven? Like it seems the goal here is `English -> Lean -> Code in whatever language` instead of just `English -> Code` but there's no way to be certain the translation step on either side of Lean has actually been done correctly. I've done a lot of experiments around this so far this year and theorem provers can certainly help provide LLMs with more context but there is no tooling to actually verify that the resulting Python fully covers the corresponding Lean that was fed in.
deleted 1y ago
[deleted]
ants_everywhere 1y ago
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.
- jsw97 1y ago
  I use the Gemini mcp and my CLAUDE.md has instructions to consult Gemini for strategy. Seems to work well. I have the lowest Claude plan so I don’t know how this would work vs Opus, for example. Separately, I have been meaning to implement a cheating detector — have run into Claude modifying problem statements, adding axioms, etc.
  - ants_everywhere 1y ago
    Okay thanks I'll try that. > have run into Claude modifying problem statements, adding axioms, etc. Same here. I've thought about creating a utility that tells Claude it has to keep going until a test exits with nonzero status. But I'm concerned Claude would just fake everything to make the test pass.
  - manmal 1y ago
    Do you need an MCP for that? Why not tell Claude to call the Gemini CLI?
    - jsw97 1y ago
      You could do that -- my understanding is that MCPs give Claude less to "think about" than having to use another program correctly, and therefore avoid context clutter. I could be wrong.
StilesCrisis 1y ago
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.
- mmaunder 1y ago
  You’re absolutely right about this.
- williamstein 1y ago
  AI is very fast at generating working self contained complicated code, which makes it too easy to establish a difficult to finish architecture.
  - deleted 1y ago
    [deleted]
  - WalterSear 1y ago
    If you don't specify otherwise, yes. With respect, if vibe coding isn't giving you the results you want, the problem is no longer the AI.
    - idontpost 1y ago
      [dead]
- lkey 1y ago
  Christ, you are so correct. > I’m about 50% of the way through the formalization plan > I think formalizing using AI was way slower than if I’d done it by hand. combined with their aversion to learning something hard alone: > I found learning Lean annoying and difficult. So I started looking for shortcuts. The author failed utterly according to their own definition of success. Moreover, how will they know they have completed the task if they don't want to fully understand what they've 'written'? The paper presents a false trichotomy: (1) go to grad school and learn to do it yourself (2) hope one of the few theorem proving experts got interested in your problem (3) give up. and the magical fourth: (4) Look Just Try Claude Code (at just $100 per month!) "got interested" is so utterly passive, I've got a fifth option. (5) Meet other people who share your interests on discord and forums and chat about the problems you are trying to solve. Make them interested! Nerd snipe them! Make friends, meet colleagues and learn new things while having a genuine human experience, for free!
amelius 1y ago
I'm curious, are there programs that generate challenges for AI, and why don't we read about them? (I'm talking about regular programs, not other LLMs or GANs)
jongjong 1y ago
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.
- cmrx64 1y ago
  This issue seems hallucinated. In the real world we just update our proofs. https://sos-vo.org/node/69931 https://sos-vo.org/node/69931
  - jongjong 1y ago
    How hypocritical of someone preaching the virtues of formal proofs to be using a single example to try to prove the 'for all' case... As if it's feasible for all systems, for all requirements, under all possible financial constraints. Oh yes, I'm the LLM here. Maybe you should run your comments through your Coq proof-assistant before you post them!
    - deleted 1y ago
      [deleted]
sheepscreek 1y ago
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.
adastra22 1y ago
> 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.
felipeerias 1y ago
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.

219 points by lairv 1y ago

deleted 1y ago

[deleted]

> 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-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?"

cube2222 1y ago
This. It’s actually extremely good bang for buck now to invest more time in various linters or static checking that enforce more correctness / project-specific rules. Not only does the AI help you write the linter in 10% of a time - linters are usually fairly short scripts that are easy to test in practice, so the happy path for AI). But asking the AI “make this linter pass” after you’ve e.g. done some extensive refactors, is very effective and time-saving.

lambdaone 1y ago

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.

qayxc 1y ago
> we are going to vibe-code ourselves to chaos. To be fair, we've been doing that even without AI for the past 5 decades.

ngruhn 1y ago

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.

burakemir 1y ago

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.

AfterHIA 1y ago
You read like Alan Kay's Quora and for that I salute you comrade.
baq 1y ago
This change is happening as we speak. My work repo is now sprouting with markdowns primarily intended for agentic consumption, but it’s all dense jargon communicating requirements and important design decisions in a way which is useful to me as a software engineer. The toil of writing these specs from low level code is much lower today, because LLMs also help with that immensely.
- burakemir 1y ago
  There is a place for informal, prose specs, and I can easily agree that more people are nowadays describing their programs in English. The context here is formal specs though - adequately and precisely capturing the intended meaning (semantics) in a way that lends itself to formal verification. Interactive theorem proving is interactive because proof search is intractable; a human articulates the property they want to prove and then performs the "search". Apart from the difficulties of getting to that proof, it can also happen that all goes through and you realize that the property is not exactly what you wanted.

bnjmn 1y ago

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

baq 1y ago

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.

Tiberium 1y ago

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?

enricozb 1y ago
If it compiles, it typechecks. If it typechecks, the proof is correct. This is a consequence of the Curry-Howard correspondence [0]. From a pure mathematician's standpoint, the content of a proof is kind of (waving big hands here) irrelevant. It's more that the existence of a proof implies the theorem is true, and thus can be used to prove other theorems. Because of this "proof-irrelevance", a great foil to an LLM's propensity to hallucinate is something like Lean. In Lean, and in theorem provers oriented towards classical mathematics, the statement of the theorem being proved is what matters most. And due to Curry-Howard, the statement is equivalent to the signature/declaration of the function, which is what the human ought to verify, while Lean will verify the body. [0]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon....
- omnicognate 1y ago
  If it compiles it definitely proves something, which may or may not be what Claude tells you it proves.
- wild_egg 1y ago
  The thing I'm stuck on is that, yes, the proof is correct. But what guarantees do I have that the proof or theorem is actually representative of the program I'm trying to specify? And beyond that, what guarantees are there that the resulting end program actually adheres to either the specs or what has been proven? Like it seems the goal here is `English -> Lean -> Code in whatever language` instead of just `English -> Code` but there's no way to be certain the translation step on either side of Lean has actually been done correctly. I've done a lot of experiments around this so far this year and theorem provers can certainly help provide LLMs with more context but there is no tooling to actually verify that the resulting Python fully covers the corresponding Lean that was fed in.

deleted 1y ago

[deleted]

ants_everywhere 1y ago

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.

jsw97 1y ago
I use the Gemini mcp and my CLAUDE.md has instructions to consult Gemini for strategy. Seems to work well. I have the lowest Claude plan so I don’t know how this would work vs Opus, for example. Separately, I have been meaning to implement a cheating detector — have run into Claude modifying problem statements, adding axioms, etc.
- ants_everywhere 1y ago
  Okay thanks I'll try that. > have run into Claude modifying problem statements, adding axioms, etc. Same here. I've thought about creating a utility that tells Claude it has to keep going until a test exits with nonzero status. But I'm concerned Claude would just fake everything to make the test pass.
- manmal 1y ago
  Do you need an MCP for that? Why not tell Claude to call the Gemini CLI?
  - jsw97 1y ago
    You could do that -- my understanding is that MCPs give Claude less to "think about" than having to use another program correctly, and therefore avoid context clutter. I could be wrong.

StilesCrisis 1y ago

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.

mmaunder 1y ago
You’re absolutely right about this.
williamstein 1y ago
AI is very fast at generating working self contained complicated code, which makes it too easy to establish a difficult to finish architecture.
- deleted 1y ago
  [deleted]
- WalterSear 1y ago
  If you don't specify otherwise, yes. With respect, if vibe coding isn't giving you the results you want, the problem is no longer the AI.
  - idontpost 1y ago
    [dead]
lkey 1y ago
Christ, you are so correct. > I’m about 50% of the way through the formalization plan > I think formalizing using AI was way slower than if I’d done it by hand. combined with their aversion to learning something hard alone: > I found learning Lean annoying and difficult. So I started looking for shortcuts. The author failed utterly according to their own definition of success. Moreover, how will they know they have completed the task if they don't want to fully understand what they've 'written'? The paper presents a false trichotomy: (1) go to grad school and learn to do it yourself (2) hope one of the few theorem proving experts got interested in your problem (3) give up. and the magical fourth: (4) Look Just Try Claude Code (at just $100 per month!) "got interested" is so utterly passive, I've got a fifth option. (5) Meet other people who share your interests on discord and forums and chat about the problems you are trying to solve. Make them interested! Nerd snipe them! Make friends, meet colleagues and learn new things while having a genuine human experience, for free!

amelius 1y ago

I'm curious, are there programs that generate challenges for AI, and why don't we read about them? (I'm talking about regular programs, not other LLMs or GANs)

jongjong 1y ago

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.

cmrx64 1y ago
This issue seems hallucinated. In the real world we just update our proofs. https://sos-vo.org/node/69931 https://sos-vo.org/node/69931
- jongjong 1y ago
  How hypocritical of someone preaching the virtues of formal proofs to be using a single example to try to prove the 'for all' case... As if it's feasible for all systems, for all requirements, under all possible financial constraints. Oh yes, I'm the LLM here. Maybe you should run your comments through your Coq proof-assistant before you post them!
  - deleted 1y ago
    [deleted]

sheepscreek 1y ago

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.

adastra22 1y ago

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

felipeerias 1y ago

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.