英国王立研究所で開催された進化生物学の一般向け講演が面白そうです!

いつも紹介している英国The Royal Institutionの動画ですが、最新の動画は進化に関する最新の手法と知見をまとめていて面白そうです。ロンドンの自然史博物館の先生による講演で、最新の化石の三次元分析法を駆使して環境と進化の相互作用をどんどん明らかにしている仕事の紹介です。地球温暖化が生物の進化速度にどのように影響するかという重要な問題に関する研究も紹介されています。ネコとイヌの進化をくらべるとなぜネコはほとんど進化していないのにイヌは様々な種類に進化しているのか?恐竜の進化速度と、恐竜の子孫である鳥の進化速度をくらべると鳥の進化がおどろくほど遅いのは何故か?ワニはなんで昔からほとんど形態が変化していないのか?などなど、進化を学ぶものが一度は疑問に思うのですが、答えをきいたことが無い疑問が回答されていてとても良い動画だと思います。これは観る値打ちのある動画ですのでお勧めします。例によってLanguage reactorの機能拡張などを使って日本語訳を表示させながら視聴するのもよいですし、最後に私がはりつけているように生成AIで要約してもらったり、文字起こし用のブラウザ機能拡張たとえばGlaspで講演内容を全部書きだしてもらってそれを翻訳するのもよいでしょう。YouTube動画のAIを使った視聴法についてはこちらの過去記事のリンクをご覧ください。

AIを使ってYouTubeの科学動画(英語版など)を効率的に視聴しましょう!第2回

さて、今日紹介する動画です。埋め込んでおきます。

The hidden rule behind all evolution | with biologist Anjali Goswami
https://youtu.be/UMjoNUb2A0I

最後にGeminiによる講演の要約も貼り付けておきます。進化生物学を学んでいる大学生向けに要約してもらいました。ざっと読んでみて、面白そうだったら動画を視聴するとよいでしょう。[]内の数字は動画の再生位置を分:秒で示したものです。元の回答にはurlリンクがあったのですがそれは省いてあります。


2. 進化生物学を学ぶ大学生向けの内容要約

本講演は、生物の形態進化におけるテンポ(進化速度)とモード(進化様式)を制御する内因的要因(発生・解剖学的制約・遺伝的相関)と外因的要因(環境・気候・生態的ニッチ)の相互作用を、幾何学的形態測定学および最新のフェノミクス(Phenomics)の手法を用いて包括的に論じたものです。

Ⅰ. 発生的・機能的制約と形態多様性

アイソメトリー vs アロメトリー [09:25]
ネコ科(Felidae):頭骨の発達において成長に伴う相対比例の変化が少ない「アイソメトリー(等比成長)」を示す。また肉食への過度な適応(裂肉歯以降の臼歯の喪失)という機能的制約により、形態的・生態的進化の自由度が著しく低い。
イヌ科(Canidae):成長過程で吻部が伸びる「アロメトリー(異比成長)」を示す。この発生プロセスの柔軟性が、人工選択(ブリーディング)における劇的な形態多様化を可能にした。

Ⅱ. 形質相関と「Fly in the Tube」モデル [16:25]

* 表現型形質間には遺伝的連鎖や発生経路の共有による強い共変異(Covariance)が存在する。
* これにより、理論上可能な表現型空間(Morphospace)の大部分は占有されず、進化の軌跡は狭い領域(チューブ状)に制限される。
* この制約こそが、有袋類のフクロオオカミ(Thylacine)と有胎盤類のオオカミ(Wolf)に見られるような収斂進化(Convergence)が頻発するメカニズムである。

Ⅲ. 進化的フェノミクス(Evolutionary Phenomics / Fionomix)の展開 [23:40]

* 従来の線形計測や少数ランドマークに基づく幾何学的形態測定学(Geometric Morphometrics)から、3D表面スキャン・CTデータを活用したセミランドマーク自動配置法およびAI学習モデル(自動化パイプライン)への移行。
* 海底堆積物コア中の微化石(有孔虫)の高処理3D解析により、地質学的時間軸における気候変動に伴うリアルタイムの種分化プロセス(Speciation)の視覚化・定量化に成功 [32:00]

Ⅳ. 大進化(Macroevolution)パターンの検証

*鳥類と非鳥類恐竜の頭骨進化 [36:03]:高次元形態空間の解析結果、鳥類は非鳥類恐竜に比べて頭骨の進化速度が著しく遅い。鳥類の頭骨は「拡大した脳+クチバシ」という基本構造に特化し、摂食やディスプレー機能を他の器官や軟組織に依存しているためである。
*哺乳類の形態進化と適応放散 [39:06]:哺乳類頭骨の平均的形態(Morphospaceの中心)はキツネ型に収斂する。進化速度の分岐には、生態(水生・草食)、発達様式(早成性/晩成性)、社会性、日周性が強く寄与しており、水棲化(クジラ類)や高い社会性・早成性を持つ系統で進化速度が顕著に増大する。

Ⅴ. 気候変動と進化速度・絶滅リスク [43:12]
* 過去200億〜数億年規模の気候データ(気温および気温変化速度)と系統推定量を用いた進化モデルの適合度検証を実施。
* 多くの系統(鳥類、ヘビ、有袋類等)において、単なる環境温度の絶対値ではなく「気候変化の速度(Rate of climate change)」が形態進化のテンポを駆動する主要因となっている。
* 現在進行中の生物多様性減退速度は、地質時代最大の温暖化イベントである古第三紀始新世極大温暖化(PETM: Paleocene-Eocene Thermal Maximum)[48:56] を遥かに上回るスピードであり、第6の大量絶滅(Mass Extinction)の閾値に達しつつあることを警告している。

戦争の時の家族の話―家系図をたどろうとした話です。

孫が歴史に興味をもっているので、先祖や家系図について調べてみることにしました。

まずは私と奥さんの戸籍を役場に出かけてさかのぼって取得することにしました。役場のすいている時間を電話できいて出かけ、試しにそれぞれの父親の戸籍をいくつか取得しました。奥さんのお父さんの兄弟は、日米戦争の時には得意の英語を使って米軍放送の傍受、解析をしていたそうです。このため敗戦後は公職追放になっていたそうですが、後には大学の英語の先生になっていたのがわかりました。この人が二年ほどかけて、先祖を戸籍と、お寺の過去帳などを使って調査していたそうで、その調査によると、先祖には大河ドラマで出てくる蜂須賀小六がいるというのがわかりました。本当なら面白いので私たちのほうでも確認しようと、過去帳のあるお寺を調べたのですが残念ながら廃寺になっていました。過去帳やお墓や親戚などから調べられるかもしれないので一度調べにいってみたいものです。

私の父親の戸籍をたどっていくと、父親の一番上のお姉さんのことがわかりました。結婚して満州に移住して小さな娘さんから年頃の娘さんまで多くの子供たちと満州開拓に携わっていたそうです。私の父親が一番上の姉は戦争で亡くなった話していたのですが、国立国会図書館のデジタルコレクションで名前を探す(キーワード検索です)とヒットしました。昭和20年の敗戦にともない帰国準備をしているところを匪賊に包囲され、家族全員自害したとありました。私の家系にも満州で亡くなった人がいるのがわかりました。

この時、満州には義母もおりました。敗戦にともない、帰国するための列車の場所についてウソを教えられて迷っていたところを、親戚にみつけてもらいやっとのことで列車に乗れて大連に到着したそうです。若い娘は襲われるので、髪を丸坊主にして逃げたそうです。大連では中国人の子供の子守をしていたと聞きました。ユーピンという名前の男の子の子守をしていたといっていました。中国の人が、平和を願うという意味の名前だよと教えてくれたと話していました。多分 宇平(ユーピン / Yǔpíng)と書くのではないでしょうか。さっきGeminiにきいてみると、この名前の「宇」は宇宙や世界といった広がり、空間を意味しており、「平」は平和ですから「世界が平和であるように」「広い心を持って平穏な人生を歩むように」といった、スケールの大きな願いが込められた名前だそうです。戦争が続いた中国の人たちの平和への願いがこもった名前ですね。その子の子守をして暮らしている時、義母は八路軍の将校に求婚されたそうですが、「私は やっぱり、日本に帰りたい」といって断りました。その将校はその後も親切にしてくれて、義母に日本に帰る船が港に来たことを教えてくれた上に、荷物を運んでくれて一緒にその船まで送ってくれたのだそうです。こうした中国の人たちの善意とやさしさのおかげで無事日本に帰国できたのは嬉しいことです。当時の八路軍は、満州に侵入したソビエト連邦軍とちがって強姦などは行わない規律の正しい軍隊だったと最近読んだ本
『ソ連兵へ差し出された娘たち』
https://www.shueisha.co.jp/books/items/contents.html?isbn=978-4-08-789015-0
にも書かれていました。

さて話を私の家系にもどすと、こちらには蜂須賀小六などは先祖におらず、平民だったようです。父の兄弟姉妹の何人かは戦争で亡くなっています。祖父は敗戦後も生き延びて、役場で働いて村の歴史をまとめた本を発行する仕事をしたりしていたことがわかりました。国立国会図書館デジタルコレクションは家系調査にも役立ちますね! 祖父の父についても戸籍から名前がわかってデジタルコレクションにも名前があるのですが、同姓同名の人かどうかは、戸籍を取り直してみないとわからない状態です。そのあたりになると文化とかいう年号がでてくる、江戸時代の生まれになるので戸籍がもう廃棄されて消えている可能性が高いようです。役場のオンラインシステムではこれ以上はたどれないようでした。こちらも親戚や地元の過去帳などから調べる他ないようです。

今日は戸籍で先祖をたどった時に知ったり、思い出した先の戦争の話でした。

文献管理ソフトZoteroとGoogleのNotebookLMの連携法―Zoteroのプラグインを使う方法

文献管理ソフトZoteroとGoogleのNotebookLMが連携できたら便利です。Zoteroにあるpdfを一発で、NotebookLMにアップロードできたら自分専用の文献データで信頼できるハルシネーションなしのChatができます (無料版のNotebookLMではnotebook一つあたり50個、有料版では300個がアップロードできます)。

Zoteroのフォーラムを検索するとよい方法がありました!ブラウザはChromeかEdgeを使う必要があり、NotebookLMの言語はEnglishにしておく必要があります。

Zoteroフォーラムの次の記事をご覧ください。今年公開された機能拡張ですが活発に開発がつづいているようでおすすめです。
“NZBridge – Bidirectional sync between Zotero and Google NotebookLM”
https://forums.zotero.org/discussion/130764/nzbridge-bidirectional-sync-between-zotero-and-google-notebooklm
デモがYouTubeにでています。
NZBridge — NotebookLM Zotero Bridge | Zotero Plugin and Edge Extension
https://youtu.be/RCJhwf-Kwto

詳しいインストール法や使い方、最新版の入手はこちらのGitHubにあるのでご覧ください。

https://github.com/Rafael-Silva-Oliveira/NZBridge
NZBridgeのインストールに必要なのは:
Zotero 7.0 or later — Zoteroのプログラム本体です。こちらからダウンロード可能です。 zotero.org
ブラウザはGoogle Chrome or Microsoft Edge (version 116+) — Manifest V3 support しているブラウザで動くそうです。
あと、NotebookLMをつかうので、 Google account が必要です。

On Chrome/Edge 142+, you must allow the extension to reach Zotero on localhost: chrome://extensions → NZBridge → Details → Site settings → Local network access → Allow. See Troubleshooting if collections won’t load or syncs time out.

Note that it only works if your NotebookLM language settings is set to english.

二つのプラグインが必要です。
Zotero Plugin Runs inside Zotero, exposing your collections and items via a local HTTP server
Browser Extension Runs in Chrome/Edge, providing the popup UI and automating sync with NotebookLM
NZBridgeの最新版はこちらからダウンロードできます。
https://github.com/Rafael-Silva-Oliveira/NZBridge/releases

話題の証明支援システム LEANについての本やサイトの紹介です。

話題の証明支援システム LEANについての本やサイトの紹介です。
望月先生のABC予想の証明の正しさをチェックするプロジェクトが使っているLEANについての本が評判になっています。The Proof in the Codeという本です。
https://www.quantabooks.org/books/the-proof-in-the-code/

もともとLEANはMicrosoftのLeo de Mouraによって開発されたプログラムです。Microsoft WordやWindowsなどのプログラムのコードにバグがないか、セキュリティ脆弱性がないか、そして設計どおりに動作するかをチェックするプログラムとして開発されました。LEANはあまり使われていなかったようですが、数学者がこれが数学の証明のチェックに使えるのに気付き、現在の証明支援システムに育て上げたのだそうです。ものすごく面白い本のようで多くの人の賛辞が上のサイトにのっています。

このLEANの公式サイトはこちらです。https://lean-lang.org/

無料のエディタであるVS Codeの機能拡張としてインストールしてセットアップして使うようです。
日本語で参考になるサイトがありました。
https://aconite-ac.github.io/
こちらはLEAN関連の、日本語の情報を中心にまとめてくださっているサイトです。ご自身の哲学探究サイト『束跡』をホストしているサイトでもあるのでとても興味のもてる内容のようです。LEAN関係の部分を以下に引用しておきます。


・Theorem Proving in Lean 4 日本語訳 : Leanのチュートリアルドキュメント「Theorem Proving in Lean 4」の非公式日本語訳です。
・Leanのインストール方法・elanとLakeの使い方 : Leanのインストール方法・elanとLakeの使い方をまとめた非公式資料です。

外部リンク
日本語情報

LEAN JA : Lean言語の日本語コミュニティです。豊富なリンク集が掲載されています。Discordサーバーもあります。
Lean by Example : LEAN JA管理者の北窓氏による、Lean言語とその主要なライブラリの使い方を豊富なコード例とともに解説した日本語資料です。


英語情報もまとまっているので役立ちます。是非参考になさってください。

広中平祐さんの本、いろいろ。

今日のKindleの日替わりセールに広中平祐さんの「学問の発見」
があって499円で売っていたので購入しました。これはブルーバックス版で2018年の広中先生の序文が新しく付け加わっています。ちょうどAIの勃興する前にでたブルーバックス版です。この本の文庫版は昔読んで持っていたのですが蔵書整理で捨てました。今Kindle版であらためて読んでみると、AI時代の今だからこそ、読んでおきたい本だと思います。今日中は499円で購入できるのでよかったら買ってみてください。他に面白い話満載ですが、岡潔先生の神がかりてきな講演会の話や岡先生が、フィールズ賞を受賞することになった研究テーマの解決につながる示唆を与えてくれた話などもあります。

あと、国立国会図書館デジタルコレクションで読める広中先生の本をいくつかあげておきます。番号は前に紹介した時のものです。他の本も紹介したのですが、例の4・22事変で館内限定化されて読めなくなっています。今読める本をいくつか追加していますので読んでみてください。

368) 江崎玲於奈, 広中平祐 著『日本を語る』,毎日新聞社,1977.3. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12589479 (参照 2025-07-25)

82) 同じくフィールズ賞受賞者の広中平祐さんの発想法についての本です。
広中平祐 著『「可変思考」で創造しよう : 頭にカツを入れる超発想法』,光文社,1987.3. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12675364

536) 広中平祐 著『湧源国家論 : 豊かさの後に何を創造するのか』,PHP研究所,1988.2. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/13067283 (参照 2026-08-06)

537) 広中平祐 著『雲の如く』,旺文社,1986.1. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12256638 (参照 2026-08-06) 広中先生のお母さんについての本です。

538) 広中平祐 著『広中平祐の数学教室 : 誰でも数学が好きになれる』上,サンケイ出版,1985.10. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12608171 (参照 2026-08-06)

539) 広中平祐 著『広中平祐の数学教室 : 誰でも数学が好きになれる』下,サンケイ出版,1985.11. 国立国会図書館デジタルコレクション https://dl.ndl.go.jp/pid/12608169 (参照 2026-08-06)

糖鎖生物学・糖鎖科学の概観を得るのに最適な本がでたので紹介します。

糖鎖生物学・糖鎖科学の概観を得るのに最適の本がでました。
「未来を創るグライコサイエンス―我が国のロートマップ2025―」という本です。
これは2018年に発行されたロードマップの新版で、ページ数もずいぶん増えて分厚くなっています(写真の二冊をくらべてみてください)。また、 2023年度から開始された「ヒューマングライコームプロジェクト」の概要も第7章にまとまっています。この本は、発行元の日本糖鎖科学コンソーシアムの次のサイトから2500円のコンソーシアムへの寄付で入手できます。

http://jcgg.jp/news/roadmap/
これは糖鎖科学の全貌を知るには最もよい本ですので、是非お読みください。私も線虫の項目を書いております。

英語版も発行されていますが、とても高価(¥28,599)なので2500円で入手できる日本語版をお読みになることをすすめます。内容はほとんど同じです。
リンクはこちら。
https://link.springer.com/book/10.1007/978-981-95-7386-8
大学など所属機関で無料で読める人はダウンロードしてみるとよいでしょう。九大では読めませんでした。
Glycoscience: A Global Roadmap 2025 from Japan
Insights from the Japan Consortium for Glycobiology and Glycotechnology (JCGG)

WindowsユーザーがLinuxを動かすしくみWSLをつかったLinux入門本が無料公開されています!

WindowsでLinuxを使いたいという人むけの、入門書が無料ダウンロード可能です。
普通にUbuntuなどを使っている非Windowsユーザーにも参考になると思います。
ダウンロードには特に登録など不要で、リンクをクリックするとダウンロードできます。ただ込み合っているようで、リンクをクリックしてもつながらないことがあるようです。
509 Bandwidth Limit Exceeded
時間をおいて試してください。
本は日本仮想化技術株式会社からでいている
『WindowsユーザーのためのWSLで始めるLinux環境構築術』です。

ダウンロードリンク入り記事はこちらです。
投稿日
2026 年 7 月 29 日
著者 ishimoto
https://virtualtech.jp/2026-07-29/

こちらのツイートから知りました。

 

東京大学オープンキャンパス2026の動画の紹介です。

東大の先生たちが、高校生向けに研究を紹介してくれるオープンキャンパスの講演会の動画が今年も公開されはじめました。いくつか紹介します。


東京大学理学部オープンキャンパス2026 オンデマンド講演会「宇宙と重力の謎に挑む-理論物理学の最前線-」高橋 卓弥 特任研究員
https://youtu.be/gzt6_n0ITzI

東京大学理学部オープンキャンパス2026 オンデマンド講演会「時空を聴く、宇宙を知るー重力波でたどる宇宙論ー」度會 大貴 特任研究員
https://youtu.be/fq1p8FToSNs

あと、今日と明日開催のオープンキャンパスの講演も面白そうです。
https://www.s.u-tokyo.ac.jp/ja/event/open-campus/2026/
こちらから視聴できます。
明日のライブ配信はこちらから視聴できます。
https://www.youtube.com/live/iQSTVmWbYj4
今日のライブ配信はこちら。
https://www.youtube.com/live/cvcy-oDXfeQ

Rでサイトの表をExcel化するパッケージ、RStudioで生成AIが使えるパッケージ、グラフや図を描くtidyplotsの教科書の紹介です。

バイオインフォマティクスや統計解析に必須のプログラミング言語Rのよさそうなパッケージと本を紹介します。

ブラウザで表示している表をExcelファイルに変換してくれるパッケージです。詳しい使い方はこちら。
Rで解析:WebページやHTMLファイルの表をまとめてExcel化「html2excel」パッケージ
公開日 2026-07-30
https://www.karada-good.net/analyticsr/r-958/

次はtidyplotsの教科書の紹介です。


オンラインで無料で読める本なので、Rでグラフや図を書く際の参考書、教科書によいと思います。

RStudioと、いろんなLLM (Codex CLIとかClaude CodeとかGeminiなど)をMCPでつないで快適に使えるパッケージClaudeRも公開されています。これも便利そうです。

こちらにLLMとのつなぎ方なども詳しく解説されています。
https://github.com/IMNMV/ClaudeR

新しい、科学、工学、物理学用のAI―Lanyon AIが登場しました!

物理学に使える新しい画期的なAIが登場したそうです。Lanyon AIというものです。宣伝の文章が以下にのっています。このLanyon AIというのはMathematicaで有名なWolframの共同研究者でWolframと「新しい物理学」の研究を進めていた一般相対性理論などの研究者Jonathan Gorard(プリンストン大学)がCEOをつとめる会社が開発したものです。Lanyon AIの登場を告げる宣伝文はこちらから読むことができます。https://lanyon.ai/blog/welcome/ 
この宣伝文では、Lanyon AIという新しく開発されたAIが、科学、エンジニアリング、ミッションクリティカルなタスク(航空宇宙や原子力など)に向けた、数学的に証明された「絶対に間違えない」新世代のAIであることが強調されています。

今までのAIとの違いはというと:
今までのAIもコードやその正しさを証明するプログラムを書くことはできましたが、「実装したコード」と「正しさの証明」を別々に生成するため、両者に矛盾が生じるリスク(例:コードは「+」なのに証明は「-」になっている等のミス)がありました。Lanyon AIは、「構築段階から正しい(Correctness by Construction)」というアプローチをとっています。AIが不完全な人間の言葉でコードを書くのではなく、後述する独自の単一言語(DSL)で「仕様」を書き出し、そこから「コード」と「証明」を同時に自動生成します。もし仕様が厳密に証明できない場合は、そもそもコードが生成されないため、構造的にエラーや矛盾を起こすことが不可能になっています。

Lanyon AIの特徴は100%の構文的正確性です。
生成されるコードとデータは数学的に正しいことが証明されており、文法や仕様と実装の不一致といったミスを犯すことが「数学的に不可能」です。そのため少しの計算ミスも許されない宇宙開発、航空宇宙工学、クリーンエネルギーなどの分野において、信頼できる物理シミュレーションや計算基盤を提供できます。また、圧倒的なスピードと低コストも大きな特徴です。従来の最先端AIモデルと比べて、ほんのわずかな計算コストとトークン数で動作します。AIは数十行の仕様を書くだけでよく、それをシステムが一瞬で数万行のコードや証明に拡張するため、1秒間に数千行の正しい数学的証明を書くほどの超高速処理が可能です。
この宣伝文での Neurosymbolic approach(ニューロシンボリック・アプローチ)というのは、「ニューラルネットワーク(昨今のAI)」と「シンボリックAI(昔からの記号的・論理的AI)」のいいとこ取りをしたハイブリッド方式のことです。これまでのLLM(AI)は、アイデアを出したり文章を作ったりする「創造性」は豊かですが、計算や論理的思考においては嘘(ハルシネーション)をつくことがありました。一方、昔ながらのプログラム(シンボリック)は「創造性」はゼロですが、決められた計算や論理ルールは「絶対に間違えない」という特徴があります。Lanyonはこの両方を組み合わせ、「AI(LLM)がクリエイティブにアイデアや仕様を提案し、それをルールベースのアルゴリズム(シンボリック)が厳格に計算・証明して形にする」という仕組みを実現しています。LEANやRocq, Agdaなどという証明支援システムを利用してチェックするようです。

また、この宣伝文にあるDomain Specific Language (DSL:ドメイン特化言語)というのは、何でもできる汎用的なプログラミング言語(PythonやC++など)ではなく、「特定の分野(ドメイン)の目的を達成するためだけに作られた専用の言語」のことです。Lanyon AIは、数学や物理学を記述するためだけに特化した独自の言語(DSL)を持っています。この言語は非常に洗練され、情報が凝縮されているため、AIはこのDSLを使ってたった「数十行」の短い指示(仕様)を書くだけで済みます。汎用言語でダラダラと長いコードを書く必要がないため、AIが処理を間違える隙がなくなり、結果として超高速かつ低コストな処理が可能になっています。注意点としては、宣伝文の注釈にもある通り、Lanyon AIが保証しているのは「仕様と実装が100%一致する(構文的な正確性)」という点であり、「人間の曖昧な意図を完璧に汲み取れるか(意味的な正確性)」については現在も研究中とのことです。

こちらのGitHubには6つほど、Lanyon AIの応用例がのっています。
https://github.com/lanyonai

たとえば以下のツイートをご覧ください。
オイラー方程式の研究例ですが、「人間なら数ヶ月から数年かかるであろう『完璧に証明されたプログラムと数学的証明』の構築を、たった3分弱で終わらせたそうです。
1次元(1D)、2次元(2D)、3次元(3D)の空間における「等温オイラー方程式」と「完全な圧縮性オイラー方程式」を解くプログラムを、すべて合わせて約179秒で生成しました。1つの条件につき、わずか13秒〜54秒しかかかっていません。また単に動くコードを書いただけではなく、そのコードが物理法則に対して「絶対に間違っていない」ことを証明するためのコード(Lean 4という定理証明言語)を10,750行も生成しました。これには270の定義と156の定理が含まれています。さらに証明だけでなく、実際にシミュレーションを動かすためのC言語のコードを6,876行生成しました。このC言語コードは上記のLean 4によって「端から端まで正しさが証明(End-to-end formally verified)」されているものです。
つまり、「超高速・大ボリューム・バグ率0%」という、従来のプログラミングやAIでは到底不可能な離れ業をやってのけたという例のようです。