LeanLinkとLeanAssistによるMathematicaとLeanのブリッジ

詳細情報

日時	2026年11月7日 22:00 - 22:40
テーマ	LeanLinkとLeanAssistによるMathematicaとLeanのブリッジ
発表者	いつものおねえさんさん
集会名	「計算と自然」集会
発表資料	リンク

Wolfram/LeanLinkにより、LeanをMathematicaから使えるようになりました。Mathematicaは、自動推論に適した形式の座標非依存の総合幾何学的シーンの記号表現をサポートし、幾何学的推論と、可視化のための関数を備えているので、初等幾何の定理を記述して図示するとともに、Mathematica で証明書を探し、Leanで検証するLeanAssistをFableさんに書いてもらいました。これはLeanを学習する教材として有用かもしれない、という内容を紹介します。

「計算と自然」集会の他の発表もチェック！

35 思考のための杖、AIと二人羽織で生きていくための方策と現状

34 SpatialMicをMathematicaにつなぐ--あるいは軌道電子とアンビソニック音場について

33 論文紹介: 電気活性ポリマーハイドロゲルは、シミュレートされたゲーム環境に身体化されたとき創発的な記憶を示す

32 Spiking Neural NetworkとDaito Manabeの「FPGAに神経回路を置く」についてしらべてみた

第31回今年度後半の「計算と自然」関連のリアルイベントについて

Vket技術学術WEEKの振り返りと雑談

「計算と自然」集会の開催情報・参加方法

「計算と自然」集会

開催日: 2026年11月7日

開催時間: 22:00 - 23:00

開催曜日: 土曜日

開催周期: 隔週 (第1第3週)

自然計算は、「自然の中で観察される計算過程と、自然に触発された人為的計算を扱う研究分野」とされています。自然計算について学び、関連する話題を気軽に話し合うことが目的の集会です。 2025年4月開講の放送大学大学院のラジオ講座 BS531ch「計算と自然'25」という分野を概観する科目と連動しています(テキスト「計算と自然」 (放送大学教材) 各オンライン書店で予約受付中)。この科目の全15回の各回のトピックを第1第3土曜日に日替わりで取り上げていきます(隔週開催のため放送日からは少しずつ遅延します)。議論が盛り上がったら、2回にわたって取り上げるかもしれません。事前に放送を聴いていれば話題に参加しやすいですが、予備知識なしでも問題ないです。内容の解説からSF的な雑談まで、自然の中で観察される「変な計算」に少しでも興味がある方はぜひ。