The key is to make general intelligence, and train models in regimes that generalize well among many domains, rather than just a bunch of math proof tricks that don't generalize.

I think LLMs have demonstrated tons of generalization already, but I concede that being good at theorem provers don't automatically translate into being good at other forms of programming and vice versa. But the labs should probably focus on generalizing rather than optimizing for each subfield of programming individually.

Also as an aside, I meant that the use of theorem provers for proving theorems is just programming, that is, Lean, Rocq etc. are programming languages. They are functional programming languages and they invoke Curry-Howard as a reason for them to work, like, at all. And that's why their reasoning is essentially intuitionistic