Maybe (for humans the two often go together), but what's the hypothesis behind assuming it will do the one and not the other? It seems like a very specific and arbitrary bet, not much unlike betting that AI will be able to learn English but not French.

▲

creata a day ago | parent [-]

I'm probably being naive here, but with theorem proving, if you have a problem then you can check whether a given solution is correct, letting people make things like AlphaProof, no? I would think that the open-endedness of software development in general would complicate that.

	▲	pron 21 hours ago \| parent [-]
		In general, problems whose solutions are easily checkable are not necessarily easily solvable, and the difficulty of finding the proof also depends on how the software is written, which is why humans, at least, don't try to prove arbitrary programs correct, but write the program and the proof together. But regardless, the tools involved are really not very complicated. While it's possible, I find it hard to justify betting on AI being able to prove a 100KLOC-10MLOC program correct while not being able to write a 10KLOC tool well enough.