What about formal proofs? Don't we expect LLMs to help there, in a more "blue team" role? E.g. when a mathematician talks about a "technical proof", enumerating cases in the thousands, my impression is that LLM would save some time, and potentially help mathematicians focus on the actually hard (rather than tedious) parts.

Formal verification and case automatikn can be done automatically anyway without a mathematician hand checking each case.

For an old example that predates LLMs, see the four color theorem.

A computer can be helpful for enumerating cases and similar mechanical work. But an LLM specifically would be a terrible way to do this.