Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust

Human review remains essential even with AI-assisted verification: The framework requires humans to review problem specifications and execution models separately from machine-checked proofs, recognizing that automated verification alone cannot guarantee an algorithm solves the intended problem—only that the computation is mathematically correct.

Resource claims need independent validation: The paper highlights a critical gap where "machine-checked proofs alone cannot guarantee that...resource claims match the verified computation," meaning humans must separately verify that quantum algorithms will actually run within practical hardware constraints.

Reusable verification components reduce review burden: Once the shared Lean-QuantumAlg framework was audited, less than 1% of each algorithm's code required human review across nine different quantum algorithms (including attacks on RSA-2048 and P-256), demonstrating how trustworthy building blocks can scale AI-assisted development.

The "Algorithm-Solves-Problem" contract clarifies responsibilities: By binding correctness, success probability, resource bounds, and quantum state restoration into a single verifiable contract, the framework makes explicit what is machine-checked versus what requires human judgment, improving transparency in AI-generated quantum algorithms.

This approach enables scalable discovery while maintaining auditability: The framework provides a pathway for AI agents to develop quantum algorithms at scale while keeping human oversight practical, rather than requiring line-by-line review of every AI-generated algorithm.