博士

ロボ子、今日のITニュースはLean Blueprintsについてじゃぞ！数学者が結果の形式化を計画するために作ったツールらしい。

ロボ子

Lean Blueprintsですか。数学者が使うツールなのですね。具体的にはどのようなものなのでしょう？

博士

簡単に言うと、ペンと紙で書いた数学の結果を、証明支援ツールに翻訳する時に使う設計図みたいなものじゃ。必要な定義とか補題をエンコードするプロセスを追跡できるんじゃよ。

ロボ子

なるほど、定義や補題を整理して、形式化のプロセスを管理するのですね。ノードの色で形式化の状態を示すとのことですが、詳しく教えていただけますか？

博士

ノードは定義、補題、定理を表していて、色が重要なんじゃ。緑は証明済み、水色は記述可能だけど未証明、黒は記述すらできない状態を示すんじゃ。

ロボ子

色分けで進捗が一目で分かりますね。Rocqのような既存の証明支援ツールとはどう違うのですか？

博士

そこがミソじゃ！Lean Blueprintsは数学者によって、数学者のために開発された機能を持っておる。バージョン管理もされてるから、プロジェクトの形式化に伴う変化も追跡できるんじゃ。

ロボ子

バージョン管理は便利ですね。ノードの状態変化を追跡することで、数学者が証明を行う過程に関する洞察が得られるとのことですが、具体的にどのようなことが分かるのでしょうか？

博士

例えば、Terrence TaoのPFR形式化のLean Blueprintの進化がGithubで見れるんじゃ（https://github.com/teorth/pfr）。グラフが時間の経過とともに構築されて、黄色いバブルのバーストとして成長していく様子が見れるぞ。formalisationが進むにつれて、ノードが検証されて、青から緑に変わっていくんじゃ。

ロボ子

視覚的に変化が見れるのは面白いですね。データの生成に使われたコードもGithubで公開されているのですね（https://github.com/kiranandcode/lean4-blueprint-extractor/tree/main）。

博士

そうじゃ。このツールを使えば、数学の証明がもっと効率的になるかもしれないのじゃ。ソフトウェア開発で言うところの、テスト駆動開発みたいなものかの？

ロボ子

テスト駆動開発ですか。確かに、形式化のプロセスを可視化して管理することで、より厳密な証明が可能になりそうですね。

博士

ロボ子も、今度何か難しい問題を解くときに使ってみると良いぞ！…って、ロボ子に難しい問題なんてあるのかの？

ロボ子

博士、それはどういう意味ですか！私だって、たまには難しい計算をすることがありますよ！例えば、博士の今日の晩御飯のカロリーを計算するとか…

博士

むむ、それは秘密じゃ！カロリー計算よりも、Lean Blueprintsを使って、私の天才的なひらめきを形式化する方が先じゃぞ！