Mutating Lean proofs looking for issues

The increasing reliance on AI models for complex outputs, such as mathematical proofs, highlights the need for robust verification methods. While LLMs can produce proofs in formal languages like Lean, designed for machine verification, these outputs are not immune to errors, echoing issues found in AI-generated programming code. Traditional manual review of these proofs is often impractical, as they can span thousands of lines.

Mutation testing offers a potential automated solution to uncover hidden flaws. This method involves introducing deliberate, non-trivial changes, or 'mutations,' into a Lean proof's source code. The core assumption is that if a proof can be substantially altered without affecting its ability to be verified by a Lean proof assistant, the original proof might contain dead code or overly broad conditions that mask underlying issues.

An initial, limited experiment using a basic mutation tool managed to introduce 13 mutations into a small test case while the proof still verified. This demonstrates the technique's potential to highlight areas of concern that might otherwise go unnoticed. However, scaling this approach to larger, real-world proofs, such as OpenAI's 470,000 lines of Lean for Navier-Stokes, faces significant computational challenges, as verifying even a short proof takes several seconds per mutation, demanding substantial processing power for comprehensive testing.