証明補助装置
RocqIDE での対話型証明セッション。左側に証明スクリプト、右側に証明状態が表示されます。

コンピュータサイエンスと数理論理学において、証明支援システム（Proof Assistant）または対話型定理証明器（Interactive Theorem Prover）は、人間と機械の協働による形式的な証明の開発を支援するソフトウェアツールである。これは、人間が証明の詳細を保存し、いくつかの手順をコンピュータが提供する、ある種の対話型証明エディタやその他のインターフェースを含む。多くの証明支援システムは、各推論ステップをチェックする小さな信頼できるカーネルを中心に構築されており、高レベルの証明手順（タクティクスなど）は証明の構築を支援する。このアーキテクチャはLCFアプローチの特徴であり、後のいくつかのシステムに影響を与えた。[ 1 ] [ 2 ]

この分野における最近の取り組みとしては、これらのツールに人工知能を利用して通常の数学の形式化を自動化することである。[ 3 ]

歴史

1967年にニコラス・ゴバート・デ・ブリュインによって開発されたAutomathは、最初の証明チェッカーであり、プログラムと証明の間のカリー・ハワード対応を利用した最初のシステムであると考えられています。[ 4 ] 1970年代には、LCFファミリーが、証明チェックのための小さな信頼できるコアとユーザーがプログラム可能な証明手順を組み合わせたアイデアを導入しました。この設計は後にHOLやIsabelleなどのシステムに影響を与えました。[ 1 ]

システム比較

名前最新バージョン開発者実装言語特徴
高階論理依存型小さなカーネル証明の自動化反射による証明コード生成
ACL28.3マット・カウフマン、J・ストロザー・ムーアコモンリスプいいえ未入力いいえはいはい[ 5 ]すでに実行可能
アグダ2.6.4.3 [ 6 ]ウルフ・ノレル、ニルス・アンダース・ダニエルソン、アンドレアス・アベル（チャルマーズとヨーテボリ）[ 6 ]ハスケル[ 6 ]はいはい[ 7 ]はいいいえ部分的すでに実行可能
アルバトロス0.4ヘルムート・ブランドルOCamlはいいいえはいはい未知まだ実装されていません
クソ*リポジトリマイクロソフトリサーチとINRIAクソ*はいはいいいえはいはい[ 8 ]はい
HOLライトリポジトリジョン・ハリソンOCamlはいいいえはいはいいいえいいえ
HOL4カナナスキス-13（またはレポ）マイケル・ノリッシュ、コンラッド・スリンド他標準MLはいいいえはいはいいいえはい
イドリス2 0.6.0エドウィン・ブレイディイドリスはいはいはい未知部分的はい
イザベルIsabelle2025（2025年3月）ラリー・ポールソン(ケンブリッジ)、トビアス・ニプコウ(ミュンヘン)、マカリウス・ウェンゼル標準ML、Scalaはいいいえはいはいはいはい
傾くv4.23.0 [ 9 ]レオナルド・デ・モウラ( Microsoft Research ) C++、リーン はい はい はい はい はい はい
レゴ1.3.1ランディ・ポラック（エディンバラ）標準MLはいはいはいいいえいいえいいえ
メタマスv0.198 [ 10 ]ノーマン・メギルANSI C
ミザール8.1.11ビャウィストク大学フリーパスカル部分的はいいいえいいえいいえいいえ
ンクム
ニューPRL5コーネル大学コモンリスプはいはいはいはい未知はい
PVS6.0SRIインターナショナルコモンリスプはいはいいいえはいいいえ未知
ロク9.0インリアOCamlはいはいはいはいはいはい
121.7.1フランク・フェニング、カールステン・シュールマン標準MLはいはい未知いいえいいえ未知
  • ACL2 – Boyer-Moore の伝統に基づくプログラミング言語、一階論理理論、および定理証明器 (対話型モードと自動モードの両方を備えています)。
  • Rocq (旧名: Coq ) – 数学的な主張の表現を可能にし、これらの主張の証明を機械的にチェックし、形式的な証明を見つけるのに役立ち、形式仕様の構成的証明から認定されたプログラムを抽出します。
  • HOL定理証明器– LCF定理証明器から派生したツール群。これらのシステムでは、論理的な中核はプログラミング言語のライブラリです。定理は言語の新しい要素を表し、論理的な正しさを保証する「戦略」を通じてのみ導入できます。戦略合成により、ユーザーはシステムとのやり取りを比較的少なくして、意味のある証明を作成できます。このファミリーのメンバーには以下が含まれます。
  • IMPS、対話型数学証明システム。[ 11 ]
  • Isabelleは HOL の後継となる対話型定理証明器です。メインのコードベースは BSD ライセンスですが、Isabelle のディストリビューションには、異なるライセンスの多くのアドオンツールがバンドルされています。
  • Jape – Java ベース。
  • 傾く
  • レゴ
  • Matita – 帰納的構成の計算に基づいた軽量システム。
  • MINLOG – 一次最小論理に基づく証明支援ツール。
  • Mizar –自然演繹スタイルの第一階論理とタルスキ-グロタンディーク集合論に基づいた証明支援ツール。
  • PhoX – 拡張可能な高階論理に基づく証明支援システム。
  • プロトタイプ検証システム(PVS) – 高階論理に基づく証明言語とシステム。
  • 定理証明システム(TPS) と ETPS – 単純型ラムダ計算に基づいていますが、論理理論の独立した定式化と独立した実装に基づいた対話型定理証明器です。

ユーザーインターフェース

証明支援システムの人気のフロントエンドは、エディンバラ大学で開発されたEmacsベースの Proof Generalです。

Rocqには、OCaml/ GtkをベースにしたRocqIDEが含まれています。Isabelleには、jEditとドキュメント指向証明処理のためのIsabelle/ ScalaインフラストラクチャをベースにしたIsabelle/jEditが含まれています。最近では、 Rocq用のVisual Studio Code拡張機能が開発されました。 [ 12 ] IsabelleはMakarius Wenzel氏によって開発されました。 [ 13 ] Lean 4用の拡張機能はleanprover開発者によって開発されました。[ 14 ]

形式化の範囲

Freek Wiedijkは、よく知られている100個の定理のリストの中から、定理が形式化されたものの数に基づいて証明支援システムのランキングを作成しています。2025年9月現在、定理の70%以上を形式化した証明を行っているシステムは、Isabelle、HOL Light、Lean、Rocq、Metamath、Mizarの6つのみです。[ 15 ] [ 16 ]

注目すべき形式化された証明

以下は、証明支援システム内で形式化された注目すべき証明のリストです。

定理 証明補助装置 年
四色定理[ 17 ]ロク2005
フェイト・トンプソンの定理[ 18 ]ロク2012
円の基本群[ 19 ]ロク2013
エルデシュ・グラハム問題[ 20 ] [ 21 ]傾く 2022
多項式フライマン・ルザ予想​​[ 22 ]F2{\displaystyle \mathbb {F} _{2}}傾く2023
BB(5) = 47,176,870 [ 23 ]ロク 2024

参照

注記

  1. ^ a b Gordon, Michael JC 「LCFからHOLへ：短い歴史」（PDF） . ケンブリッジ大学（コンピュータ研究所） . 2026年1月14日閲覧。
  2. ^ Gordon, Michael JC; Milner, Robin; Morris, Lockwood; Newey, Malcolm; Wadsworth, Christopher P. (1978). 「LCFにおける対話型証明のためのメタ言語」. Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '78) : 119– 130. doi : 10.1145/512760.512773 .
  3. ^ Ornes, Stephen (2020年8月27日). 「Quanta Magazine – コンピューターは数学的推論の自動化にどれだけ近づいているか？」 .
  4. ^ Geuvers, Herman (2009年7月16日). 「証明支援ツール：歴史、アイデア、そして未来」(PDF) . Sādhanā . 34 : 3–25 .
  5. ^ Hunt, Warren; Kaufmann, Matt ; Krug, Robert Bellarmine; Moore, J.; Smith, Eric W. (2005). 「ACL2におけるメタ推論」(PDF) .高階論理における定理証明. コンピュータサイエンス講義ノート. 第3603巻. pp.  163– 178. doi : 10.1007/11541868_11 . ISBN 978-3-540-28372-0。
  6. ^ a b c「agda/agda: Agdaは依存型プログラミング言語/対話型定理証明器です」。GitHub 。2024年7月31日閲覧。
  7. ^ “アグダ Wiki” . 2024 年7 月 31 日に取得。
  8. ^「反射による証明」を検索: arXiv : 1803.06547
  9. ^ 「Lean 4 Releases Page」 . GitHub . 2025年9月22日閲覧。
  10. ^「リリース v0.198 metamath/Metamath-exe」。GitHub 。
  11. ^ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier (1993). 「IMPS: 対話型数学証明システム」 . Journal of Automated Reasoning . 11 (2): 213– 248. doi : 10.1007/BF00881906 . S2CID 3084322. 2020年1月22日閲覧。 
  12. ^ "coq-community/vscoq" . 2024年7月29日 – GitHub経由.
  13. ^ Wenzel, Makarius. 「イザベル」 . 2019年11月2日閲覧。
  14. ^ 「VS Code Lean 4」 . GitHub . 2023年10月15日閲覧。
  15. ^ Wiedijk、フリーク (2025 年 9 月 22 日)。「100の定理の定式化」。
  16. ^ Geuvers, Herman (2009年2月). 「証明支援系：歴史、思想、そして未来」 . Sādhanā . 34 (1): 3– 25. doi : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 . S2CID 14827467 . 
  17. ^ Gonthier, Georges (2008)、「形式的証明—4色定理」(PDF)、アメリカ数学会誌、55 (11): 1382– 1393、MR 2463991、2011年8月5日時点のオリジナルよりアーカイブ(PDF) 
  18. ^ “Feit Thomson proved in coq - Microsoft Research Inria Joint Centre” . 2016年11月19日.オリジナルより2016年11月19日時点のアーカイブ。 2023年12月7日閲覧。
  19. ^ Licata, Daniel R.; Shulman, Michael (2013). 「ホモトピー型理論における円の基本群の計算」. 2013 第28回ACM/IEEEコンピュータサイエンスにおける論理シンポジウム. pp.  223– 232. arXiv : 1301.3443 . doi : 10.1109/lics.2013.28 . ISBN 978-1-4799-0413-6. S2CID  5661377 .
  20. ^ 「3500年かけて解明された数学の問題がついに解明」 IFLScience 2022年3月11日2024年2月9日閲覧。
  21. ^ Avigad, Jeremy (2023). 「数学と形式的転回」. arXiv : 2311.00007 [ math.HO ].
  22. ^スローマン、レイラ (2023-12-06). 」「数学の『Aチーム』が加算と集合の重要なつながりを証明」 Quanta Magazine 。 2023年12月7日閲覧。
  23. ^ 「BB(5) = 47,176,870」であることを証明した。「 . The Busy Beaver Challenge . 2024年7月2日. 2024年7月9日閲覧.

参考文献

カタログ
「 https://en.wikipedia.org/w/index.php?title=Proof_assistant&oldid=1333071088#System_comparison」から取得