#証明支援系

AIが書いたコード、数学的に証明できるか：Leanとともに行う形式検証の実践

AIコーディングツールが生成したコードの正確性を保証するために、Leanのような証明支援系を活用する半自動形式検証パイプラインとその限界を考察します。