Agreed that confirming “This proposition has been faithfully translated to Lean” matters. As a side note, though, this is an area where LLMs used interactively

Agreed that confirming “This proposition has been faithfully translated to Lean” matters. As a side note, though, this is an area where LLMs used interactively can be helpful. Also in the case of these recent counterexamples turning up, we have good qualitative evidence that this pathway is effective.