そもLeanに翻訳するのが難しいと言われるといつ終われるのか分からんな


【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
https://www.youtube.com/live/b6JlM_nrM3M


━━ LANAプロジェクト（IUT理論の検証プロジェクト）の進捗状況については、1時間03分30秒頃から語られています。加藤先生と川上氏が、プロジェクトの中間発表の内容や、現在の到達点について詳しく説明しています。

•判断の保留: 現時点では理論が正しいか間違っているかを断定する段階には至っておらず、引き続き検証が必要な状態であること（1:03:32-1:04:10）。
•言語化の壁: コンピュータ言語（Lean）へ翻訳するための前提となる人間側の理解において、まだ解明すべき難所があること（1:04:11-1:07:25）。


━━ 遠アーベル幾何学の内容をコンピュータ言語である Lean に落とし込むプロジェクトについての話は、1時間36分49秒頃から始まります。

このパートでは、IUT理論の根幹をなす遠アーベル幾何学を計算機上で扱うことの難しさと、なぜそれが重要なのかについて以下の点が語られています：

• IUT理論と計算機科学の接点: IUT理論自体は非常に難解でキャッチーな話題ですが、その土台となる遠アーベル幾何学を Lean に落とし込むこと自体が、数学研究における新しい手法として重要であると説明されています (1:36:51-1:37:04)。
• プロジェクトの意義: IUT理論を検証する過程で、この基盤となる理論をコード化することは、現代数学の新しい検証手法としての大きな実績になるという議論がなされています (1:37:05-1:37:14)。