Palomar：Leanで検証された数学の登録簿が公開
Palomar: A registry of Lean verified mathematics
Terence Tao氏は、Leanで形式化された数学の証明を登録するためのレジストリ「Palomar」の開設を発表した。Palomarは、AI生成の証明が増える中で、証明が実際に主張を検証しているかを確認する仕組みを提供する。登録には、チャレンジファイル、ソリューションモジュール、formalization.yamlファイルが含まれ、機械的なチェックとLLMによる意味的整合性のチェックが行われる。査読付きジャーナルではないが、証明の信頼性を高めるための一歩となる。
Palomarは、Leanの証明のためのプレプリントサーバーの類似物を意図している。
HNでの議論
39- sva_
> 提出プロセスは徹底しているが、達成可能だ。試しに、私は自分の最近の形式化を提出することに成功した [...]
こういうの、なんだか愛らしい。彼が「私にさえできるんだから、あなたにもできるはず」と言っているように聞こえるのが。彼がおそらく現在生きている中で最も多作な数学者であることを無視して。
数年前、私は形式的に検証可能な数学の証明の一種のブロックチェーンがあると面白いかもしれないと提案したが、ゲーデルの不完全性定理のために無駄な試みだと言う人々にすぐに否定された。
数学の証明のライブラリを計算機で作成するという大きな問題は、まだ、証明するのが自明な役に立たない定理を無限に生成できるかもしれないことだと思うが、この登録簿は手動で審査されているのだろう。数学には強い帰納的バイアスがあり、人間がどの公理系、定理、定義が私たちにとって興味深いかをまだ決定している。
しかし、証明する方法は、おそらく人生の何年かを捧げる努力として、すぐに時代遅れになると思う。
- JuniperMesos
> パロマーが意図するもののゼロ次近似は、Leanの証明のためのプレプリントサーバーの類似物です。より正確には、パロマー（天文台にちなんで名付けられた）は、Leanコードを含む外部のGithubリポジトリ（より正確には、特定のGithubコミットによって表されるそのようなリポジトリの「スナップショット」）の登録簿であり、そのような形式化の現在のベストプラクティスに準拠しています。
テレンス・タオは、不正確かつ不正確に、人気のあるgitリポジトリホスティングサービスの名前「Github」を、オープンソースのバージョン管理システム「git」の同義語として使用している。おそらく彼はソフトウェアのバージョン管理にある程度精通しているが、コンピュータプログラミングの専門家ではないからだろう。あるいは、彼はその区別を完全に理解しており、パロマーはGitHubでホストされているgitリポジトリでのみ機能するように書かれており、タオはそれを正確に説明している。どちらの可能性も残念だ。私は、分散型バージョン管理システムのホスティングにおけるGitHubの事実上のマインドシェア独占を好まない。
- bramhaag
Leanは、Isabelleが何十年も持っているもの（https://isa-afp.org/）を、より悪い方法で再発明し続けているように見える。これがGitHubに依存する理由はない。
- dwheeler
とてもクールだ。metamathコミュニティは結果を集中化する傾向があるので、その同等物は単にこれだ：
- cbondurant
ハードなGitHub依存が「これを世に出す最も簡単な方法だった」と言い訳できることを願うだけだ。長期的には良い解決策ではない（単一障害点、GitHubはますます信頼性が低く嫌われている、別のフォージやリポジトリソースに既にいる人々はどうするのか？）が、少なくともいくつかの問題は解決している。そうでなければ厄介だったであろう問題（提出の最低基準、アイデンティティとスパム管理をGitHubに外部委託するなど）。
そして、検証の基準が明示的にかなり弱いと述べられているので、これは、平凡な形式化された証明の80パーセンタイル未満をふるい落とすことができる専門の検索エンジンとして概念化するのが最善だろう。対象読者は、最終的な20%について自分で判断できるプロの数学者だ。
また、数学者ではないがLeanがただ素晴らしいと思う人として、いつかざっと目を通したいものかもしれない。私には役に立たないが、学ぶのは楽しい。