ここ数ヶ月、様々な古い結果や新しい結果のAI生成証明が急増しており、その中には証明支援言語Leanで形式化されたものもあります。しかし、与えられたLeanリポジトリが実際に主張されている命題を証明していることを確認することは、特に専門家ではない読者にとっては、ある程度自明ではありません。