HyperAIHyperAI

Command Palette

Search for a command to run...

AI協働で完成した数学証明の新展開:ChatGPTとAristotleが生み出したLean検証済み論文の実態

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

関連リンク

<p>Meanwhile, with further prompting, ChatGPT was also able to adapt the argument to handle large ? as well as small ?, thus finally producing a new result in the spirit of the intended question <a href="https://drive.google.com/file/d/1xRw8_o2C8HwmxMDnBR5OJlxXaW7jlYbz/view?usp=sharing" target="_blank" rel="nofollow noopener" translate="no"><span class="invisible">https://</span><span class="ellipsis">drive.google.com/file/d/1xRw8_</span><span class="invisible">o2C8HwmxMDnBR5OJlxXaW7jlYbz/view?usp=sharing</span></a> . Interestingly, the proof contained some minor errors in it, but the AI tool Aristotle was able to automatically repair these gaps and produce a Lean-verified proof.</p><p>At this point, a third particiant ran Aristotle again on the existing Lean proof to provide a shorter version, which a different participant then input into a lengthy back-and-forth ChatGPT session <a href="https://chatgpt.com/share/695e7cbd-605c-8010-809b-ccba75560c76" target="_blank" rel="nofollow noopener" translate="no"><span class="invisible">https://</span><span class="ellipsis">chatgpt.com/share/695e7cbd-605</span><span class="invisible">c-8010-809b-ccba75560c76</span></a> to turn it into a much more fully fleshed article that described not just the proof itself, but its connection with prior literature and with a tighter narrative structure. This resulted in a new writeup of the proof <a href="https://drive.google.com/file/d/1MRQfcHhrYMfMTvlZcMC3zEK7aOrUyHiQ/view?usp=sharing" target="_blank" rel="nofollow noopener" translate="no"><span class="invisible">https://</span><span class="ellipsis">drive.google.com/file/d/1MRQfc</span><span class="invisible">HhrYMfMTvlZcMC3zEK7aOrUyHiQ/view?usp=sharing</span></a> that had less of the feel of a generic AI-produced document, and which I judge to be at a level of writing within ballpark of an acceptable standard for a research paper, although there is still room for further improvement. (I review this text at <a href="https://www.erdosproblems.com/forum/thread/728#post-2852" target="_blank" rel="nofollow noopener" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">erdosproblems.com/forum/thread</span><span class="invisible">/728#post-2852</span></a> ). (4/5)</p>
陶哲轩陶哲轩
AI協働で完成した数学証明の新展開:ChatGPTとAristotleが生み出したLean検証済み論文の実態 | 人気の記事 | HyperAI超神経