AI協働で完成した数学証明の新展開:ChatGPTとAristotleが生み出したLean検証済み論文の実態
さらにプロンプトを繰り返すことで、ChatGPTは大規模な変数と小規模な変数の両方に対応するよう論証を修正し、意図された問題の精神に沿った新たな結果を導き出した。その結果、Googleドライブに公開された証明書(リンク)が生成された。この証明にはわずかな誤りが含まれていたが、AIツール「Aristotle」がこれらのギャップを自動で補い、Leanで検証可能な証明を生成した。 その後、第三者がAristotleを再び実行し、既存のLean証明をさらに短縮。その短縮版は、別の参加者がChatGPTと長時間にわたるやり取りを重ね、証明の内容に加え、既存の研究文献との関連性や、より緊密な物語構成を加えることで、大幅に洗練された論文風の文章に仕上げた。このプロセスを経て、最終的に公開された新証明文書(リンク)は、機械的・一様なAI生成文の印象を大幅に減らしており、研究論文としての水準に近い完成度に達していると評価できる。ただし、さらなる改善の余地は残されている。 この成果は、AIが単なる補助ツールとしてではなく、複数の段階を経て共同研究の一部を担う可能性を示している。特に、人間の知的介入とAIの補完的活用が組み合わさることで、質の高い学術的成果が創出可能であることが実証された。詳細なレビューは、Erdős問題フォーラムにて公開されている。
