https://note.com/katobungen/n/n20ae018293e6?sub_rt=share_pb
OpenAIの数学リポジトリにLANA-agentsが現れた日
加藤文元
2026年10月16日

2026年10月6日、OpenAIが、未公開の社内AIモデルによって生成された700本を超える数学の原稿を、関連するLeanコードなどとともにGitHub上に公開した。その内容に数学者たちの関心が集まる中、我々LANAのメンバーは、公開されたopenai/mathのlean/lakefile.leanというLeanコードに、「lana-agents」という文字列が11件あることに気づいた。我々がIUT理論の形式化のために設けたGitHub上の名前が、OpenAIの研究環境にも現れていたのである。

このことから、IUT理論の検証はAIによって可能なのか、そしてOpenAIをはじめとした世界の動きはどうなっているのか、といったことについて、いくつか新しい視点を得ることができたので、ここに少し打ち明けようと思う。

ここから先は
3,581語