Palomar: Leanで検証された数学の登録所

最近数ヶ月、様々な古今東西の定理に対するAI生成証明が急増しており、その一部は証明支援言語Leanで形式化されています。しかし、与えられたLeanリポジトリが実際に主張された命題を証明しているかを確認することは、Leanの専門家でない聴衆にとっては、ある程度自明ではありません。まず、主張されたLeanの形式的命題に型チェックが通る証明が存在すること、証明に「不正行為」（追加公理の追加など）が含まれていないこと、そして形式的命題が主張された結果の非形式的な記述と（意味論的な意味で）一致していることを確認する必要があります。 この状況にいくらかの明確さをもたらすため、Lean FROおよびICARMによってインキュベートされたイニシアチブであるLeanで検証された数学の登録所Palomarが、現在提出を受け付けていることを発表できることを嬉しく思います。私は、Jeremy Avigad、Matthew Ballard、Jaume de Dios、Nestor Guillen、Bryna Kra、Kim Morrison、Ravi Vakil、Akshay Venkateshと共に、科学諮問委員会のメンバーを含む、この登録所のいくつかの役割を担っています。Palomarの詳しい動機はここ、Palomarに関するさらなる情報はここで見つけることができます。 Palomarが意図するもののゼロ次の近似は、Lean証明のためのプレプリントサーバーのアナログです。より正確には、Palomar（天文台にちなんで名付けられました）は、Leanコードを含む外部Githubリポジトリ（より正確には、特定のGithubコミットによって表されるそのようなリポジトリの「スナップショット」）の登録所であり、そのような形式化のための現在のベストプラクティスに従っており、特に以下のものを含んでいます。 「チャレンジファイル」：Leanで書かれた、主張された結果の短く人間が読める記述が含まれています。 「ソリューションモジュール」：チャレンジファイルで主張された結果の（任意の長さの）証明が含まれています。 「formalization.yaml」ファイル：非形式的な言語で結果を記述し、さらに他の関連メタデータや開示情報も含まれています。（リポジトリには、ここに省略するいくつかの追加の技術的要件もあります。） リポジトリのスナップショットがPalomarに提出されると、(a) ソリューションモジュールが型チェックを通り、チャレンジファイルで主張された結果と正確に一致する証明を提供すること、および (b) formalization.yaml ファイルの非形式的な結果の記述が、チャレンジファイルで主張された結果と一致するように見えること、そしてリポジトリが登録エントリに必要な様々な最小基準を満たしていること、の両方がチェックされます。 最初のチェック(a)は、LeanツールComparatorを使用して純粋に機械的に行われます。2番目のチェック(b)は、大規模言語モデルによって実行される非決定的なものです。リポジトリが両方のチェックに合格すると、Palomarに登録できます。 チェック(a)と(b)は、提出物の新規性、関心度、正確性に対する適切な人間のピアレビューが得られるものよりもはるかに不足していることを強調する価値があります。特に、Palomarは査読付きジャーナルではありません。 提出プロセスは徹底的ですが、達成可能です。テストとして、私は最近のSendov予想の証明の形式化をPalomarに正常に提出することに成功しました。また、古い形式化もまもなく登録所に提出する予定です。いずれにせよ、登録所は現在、古今東西の結果の形式化を受け付けています。 提出物（人間が生成したもの、AIが生成したもの、またはその両方の混合物）を歓迎します。提出を開始する前に、ここにある（やや詳細な）指示をお読みください。（ただし、現代のAIエージェントは提出の機械的な詳細の支援に非常に役立ちますが、人間のレビューは依然として強く推奨されることを指摘しておきます。） Palomarに関する議論とフィードバックは、このZulipチャンネルで行われます。 共有: 印刷 (新規ウィンドウで開く) 印刷 友達にリンクをメール (新規ウィンドウで開く) メール その他 Xで共有 (新規ウィンドウで開く) X Facebookで共有 (新規ウィンドウで開く) Facebook Redditで共有 (新規ウィンドウで開く) Reddit Pinterestで共有 (新規ウィンドウで開く) Pinterest いいね 読み込み中... 最近のコメント Terence Tao on Notes on the classification of… Anonymous on A digestion of the Jacobian co… Anonymous on Notes on the classification of… Karim Adiprasito on A digestion of the proof of Se… Anonymous on A digestion of the proof of Se… Anonymous on Notes on the classification of… Anonymous on The blue-eyed islanders puzzle… dutifullyb3c31ab42c on A digestion of the proof of Se… Anonymous on A digestion of the proof of Se… Anonymous on Career advice Teng Zhang on A digestion of the proof of Se… Teng Zhang on A digestion of the proof of Se… Teng Zhang on A digestion of the proof of Se… Anonymous on A digestion of the Jacobian co… Teng Zhang on A digestion of the proof of Se… トップ投稿 A digestion of the proof of Sendov's conjecture A digestion of the Jacobian conjecture counterexample Career advice Palomar - a registry of Lean verified mathematics On writing Books About Does one have to be a genius to do maths? A partial digestion of the HRT counterexample 247B, Notes 2: Decoupling theory アーカイブ 2026年8月 (3) 2026年7月 (9) 2026年6月 (3) 2026年5月 (1) 2026年3月 (4) 2026年2月 (3) 2026年1月 (4) 2025年12月 (5) 2025年11月 (5) 2025年9月 (1) 2025年8月 (3) 2025年7月 (1) 2025年6月 (2) 2025年5月 (5) 2025年4月 (2) 2025年3月 (1) 2025年2月 (3) 2025年1月 (1) 2024年12月 (3) 2024年11月 (4) 2024年10月 (1) 2024年9月 (4) 2024年8月 (3) 2024年7月 (3) 2024年6月 (1) 2024年5月 (1) 2024年4月 (5) 2024年3月 (1) 2023年12月 (2) 2023年11月 (2) 2023年10月 (1) 2023年9月 (3) 2023年8月 (3) 2023年6月 (8) 2023年5月 (1) 2023年4月 (1) 2023年3月 (2) 2023年2月 (1) 2023年1月 (2) 2022年12月 (3) 2022年11月 (3) 2022年10月 (3) 2022年9月 (1) 2022年7月 (3) 2022年6月 (1) 2022年5月 (2) 2022年4月 (2) 2022年3月 (5) 2022年2月 (3) 2022年1月 (1) 2021年12月 (2) 2021年11月 (2) 2021年10月 (1) 2021年9月 (2) 2021年8月 (1) 2021年7月 (3) 2021年6月 (1) 2021年5月 (2) 2021年2月 (6) 2021年1月 (2) 2020年12月 (4) 2020年11月 (2) 2020年10月 (4) 2020年9月 (5) 2020年8月 (2) 2020年7月 (2) 2020年6月 (1) 2020年5月 (2) 2020年4月 (3) 2020年3月 (9) 2020年2月 (1) 2020年1月 (3) 2019年12月 (4) 2019年11月 (2) 2019年9月 (2) 2019年8月 (3) 2019年7月 (2) 2019年6月 (4) 2019年5月 (6) 2019年4月 (4) 2019年3月 (2) 2019年2月 (5) 2019年1月 (1) 2018年12月 (6) 2018年11月 (2) 2018年10月 (2) 2018年9月 (5) 2018年8月 (3) 2018年7月 (3) 2018年6月 (1) 2018年5月 (4) 2018年4月 (4) 2018年3月 (5) 2018年2月 (4) 2018年1月 (5) 2017年12月 (5) 2017年11月 (3) 2017年10月 (4) 2017年9月 (4) 2017年8月 (5) 2017年7月 (5) 2017年6月 (1) 2017年5月 (3) 2017年4月 (2) 2017年3月 (3) 2017年2月 (1) 2017年1月 (2) 2016年12月 (2) 2016年11月 (2) 2016年10月 (5) 2016年9月 (4) 2016年8月 (4) 2016年7月 (1) 2016年6月 (3) 2016年5月 (5) 2016年4月 (2) 2016年3月 (6) 2016年2月 (2) 2016年1月 (1) 2015年12月 (4) 2015年11月 (6) 2015年10月 (5) 2015年9月 (5) 2015年8月 (4) 2015年7月 (7) 2015年6月 (1) 2015年5月 (5) 2015年4月 (4) 2015年3月 (3) 2015年2月 (4) 2015年1月 (4) 2014年12月 (6) 2014年11月 (5) 2014年10月 (4) 2014年9月 (3) 2014年8月 (4) 2014年7月 (5) 2014年6月 (5) 2014年5月 (5) 2014年4月 (2) 2014年3月 (4) 2014年2月 (5) 2014年1月 (4) 2013年12月 (4) 2013年11月 (5) 2013年10月 (4) 2013年9月 (5) 2013年8月 (1) 2013年7月 (7) 2013年6月 (12) 2013年5月 (4) 2013年4月 (2) 2013年3月 (2) 2013年2月 (6) 2013年1月 (1) 2012年12月 (4) 2012年11月 (7) 2012年10月 (6) 2012年9月 (4) 2012年8月 (3) 2012年7月 (4) 2012年6月 (3) 2012年5月 (3) 2012年4月 (4) 2012年3月 (5) 2012年2月 (5)