Writing proofs is just writing code in a niche language (that's what the Curry-Howard isomorphism is all about). Writing modular proofs with better abstractions is just writing modular code with better abstractions.
Yeah agents need to step up their programming game in general. They write too verbose code and are happy with duplicating code. This works up until the code is so big that they can't process the code base effectively.
If I had to guess, if you train agents to write better proofs (better modularized, etc), they will get better at programming in general. Or at very least, better at writing Haskell, since so many theorem provers are just sufficiently powerful functional programming languages. And if you get better at writing Haskell, you probably get a little better at writing Rust too. That's why I think this skill probably generalizes a lot.
So maybe training agents to do math will get them, like, use Creusot [0] or flux [1] or Aenas [2] to write proofs on their Rust code, and even when they don't, they will probably write code in ways that are more amenable for reasoning
[0] https://creusot.rs/
[1] https://flux-rs.github.io/
[2] https://lean-lang.org/use-cases/aeneas/
Yeah agents need to step up their programming game in general. They write too verbose code and are happy with duplicating code. This works up until the code is so big that they can't process the code base effectively.
If I had to guess, if you train agents to write better proofs (better modularized, etc), they will get better at programming in general. Or at very least, better at writing Haskell, since so many theorem provers are just sufficiently powerful functional programming languages. And if you get better at writing Haskell, you probably get a little better at writing Rust too. That's why I think this skill probably generalizes a lot.
So maybe training agents to do math will get them, like, use Creusot [0] or flux [1] or Aenas [2] to write proofs on their Rust code, and even when they don't, they will probably write code in ways that are more amenable for reasoning
[0] https://creusot.rs/
[1] https://flux-rs.github.io/
[2] https://lean-lang.org/use-cases/aeneas/