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/

Curry-Howard doesn't buy you any shortcuts to capability. Surely no expense has been spared in training models to write good (well modularized, robust, generic etc.) code, and yet they still write slop (poorly structured, overfit to specification gaps, etc.) We see the same sloppish habits in their mathematics, perhaps transported along the CH iso. So "train[ing] agents to write better proofs" seems to me like a grand challenge problem for AI research, just like getting them to write good code. It won't be solved just by noticing that the two problems are isomorphic: we'll keep getting models that are a little better at grinding out proofs, hence a little better at grinding out programs, but the abstraction wall won't magically drop in either world just because the same limited behaviors can be transported along CH.