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.