Lean-QuantumAlg：让 AI 智能体生成人类可信量子算法的框架

Lean-QuantumAlg 是一套基于 Lean 4 的量子算法形式化框架，旨在帮助 AI 智能体生成兼具正确性与资源边界保证的人类可信量子算法。该框架在 Grover 搜索以及针对 RSA-2048 和 P-256 的量子攻击等 9 个 AI 形式化算法上完成验证。在共享框架审计完成后，每个算法仅需不到 1% 的导入源代码接受语句级人工审查。