校正アシスタント

コンピュータ科学や数理論理学において、証明支援システムまたは対話型定理証明器とは、人間と機械の協働によって形式的な証明を作成するのを支援するソフトウェアツールである。これには、対話型の証明エディタ、あるいはその他のインターフェースが含まれ、人間はそれを用いて証明の探索を誘導する。証明の詳細はコンピュータに保存され、一部の手順はコンピュータによって提供される。

この分野における最近の取り組みとして、これらのツールに人工知能を使用して通常の数学の形式化を自動化する試みが行われている。^{[ 1 ]}

自動証明検証とは、ソフトウェアを用いて証明の正当性を検証するプロセスです。これは、自動推論の分野で最も発展した分野の一つです。自動証明検証は、自動定理証明とは異なり、新しい証明や定理を自ら開発するのではなく、既存の証明の形式的な動作を機械的に検証するだけです。そのため、自動証明検証の作業は自動定理証明よりもはるかに単純であり、自動証明検証ソフトウェアは自動定理証明ソフトウェアよりもはるかにシンプルに設計できます。

この小規模さゆえに、一部の自動証明検証システムはコアコードが1000行未満で済む場合があり、そのため手動による検証と自動ソフトウェア検証の両方に対応可能です。Mizarシステム、HOL Light、Metamathは、自動証明検証システムの例です。自動証明検証は、バッチ処理として実行することも、対話型定理証明システムの一部として対話的に実行することもできます。

1967年にニコラース・ゴバート・デ・ブルインによって開発されたAutomathは、最初の証明チェッカーであり、プログラムと証明の間のカリー・ハワード対応を利用した最初のシステムであるとよく考えられている。^{[ 2 ]} 1977年にLSファン・ベンテム・ユッティングはAutomathを使用して、実数の最初の形式化であるランダウの『解析の基礎』を形式化した。 ^{[ 3 ]}

1973年、ロバート・ボイヤーとJ・ムーアは、数学ではなくプログラムの検証を目的とした『LISP関数の定理の証明』を出版した。^{[ 4 ]}彼らの定理証明器は現在ACL2として知られている。

1970年代、エジンバラLCFは定理証明器のメタ言語として関数型プログラミング言語を使用するというアイデアを導入し、HOLファミリーの証明支援システムにつながった。^{[ 3 ]}

1990年代には、 Rocq （当時はCoqとして知られていた）が登場し、多くの大規模な形式化プロジェクトで利用されてきた。2010年代後半以降、 Rocqの影響を強く受けた証明支援システムであるLeanが、特に数学の形式化において、もう一つの人気のある選択肢となっている。

• ACL2は、ボイヤー・ムーアの伝統に基づくプログラミング言語、一階述語論理理論、および定理証明器（対話型モードと自動モードの両方を備える）である。
• HOL定理証明器– LCF定理証明器から派生したツール群。これらのシステムでは、論理的な中核はプログラミング言語のライブラリです。定理は言語の新しい要素を表し、論理的な正しさを保証する「戦略」を介してのみ導入できます。戦略の組み合わせにより、ユーザーはシステムとのやり取りを比較的少なくして、重要な証明を作成できます。このファミリーには以下のものが含まれます。
  • HOL4 – 活発に開発が続けられている「主要な後継」。Moscow MLとPoly/MLの両方をサポート。BSDスタイルのライセンスを採用。
  • HOL Light – 活気のある「ミニマリストフォーク」。OCamlベース。
  • ProofPower – 独自規格に移行後、オープンソースに戻った。Standard MLに基づいている。
• IMPS、対話型数学証明システム。^{[ 11 ]}
• Isabelleは対話型の定理証明器であり、他のシステムを組み込むことができます。Isabelle/HOLは最も人気のあるインスタンスで、その基盤はHOL証明器の基盤とよく似ています。その他のインスタンスには、Isabelle/ZFやIsabelle/FOL ^{[ 12 ]}などがあります。メインのコードベースはBSDライセンスですが、Isabelleディストリビューションには、さまざまなライセンスの多くのアドオンツールがバンドルされています。
• Jape – Javaベース。
• Leanは、対話型定理証明器であると同時に、関数型で依存型付けのプログラミング言語でもあります。非累積的な宇宙を用いた帰納的構成の計算に基づいています。バージョン4（2023年リリース）以降は、自己ホスティングに対応しています。数学の形式化（形式数学のための大規模で一貫性のあるライブラリを備えています）だけでなく、ソフトウェアやハードウェアの検証にも使用できます。
• レゴ
• Matita – 帰納的構成の計算に基づいた照明システム。
• MINLOG – 一階最小論理に基づく証明支援システム。
• Mizar – 一階述語論理に基づき、自然演繹のスタイルで、タルスキ＝グロタンディーク集合論を用いた証明支援システム。
• PhoX – 拡張可能な高階論理に基づく証明支援システム。
• プロトタイプ検証システム（PVS） – 高階論理に基づいた証明言語およびシステム。
• Rocq（旧名Coq） – 帰納的構成の計算に基づいた、人気の高い対話型定理証明器。
• 定理証明システム（TPS）およびETPS – 対話型定理証明器であり、単純型ラムダ計算に基づいているが、論理理論の独立した定式化と独立した実装に基づいている。

証明支援システムの一般的なフロントエンドとして、エジンバラ大学で開発されたEmacsベースの Proof Generalがありました。現在では、多くの証明システムが独自のエディタを備えています。Rocq には OCaml/ Gtkベースの RocqIDE が含まれています。Isabelle には、 jEditと文書指向の証明処理のためのIsabelle/ Scalaインフラストラクチャに基づいた Isabelle/jEdit が含まれています。さらに最近では、 Rocq ^{[ 13 ]}、Makarius Wenzel による Isabelle ^{[ 14 ]}、leanprover 開発者による Lean 4 ^{[ 15 ]}向けにVisual Studio Code拡張機能が開発されています。

Freek Wiedijk は、100 のよく知られた定理のリストのうち、形式化された定理の数に基づいて証明支援システムのランキングを維持しています。2025 年 9 月現在、定理の 70% 以上を形式化した証明を持つシステムは、Isabelle、HOL Light、Lean、Rocq、Metamath、Mizar の 6 つだけです。^{[ 16 ] [ 17 ]}

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

• 自動定理証明– 自動推論および数理論理学のサブ分野 
• コンピュータ支援証明– 少なくとも部分的にコンピュータによって生成された数学的証明 
• 形式検証– 特定のアルゴリズムの正しさを証明または反証すること 
• Prover9は、一階述語論理と等式論理のための自動定理証明器です。
• QEDマニフェスト– 全ての数学的知識を網羅したコンピュータベースのデータベースに関する提案 
• 理論による充足可能性– コンピュータサイエンスで研究される論理問題 

• Barendregt, Henk ; Geuvers, Herman (2001). "18. 依存型システムを用いた証明支援" (PDF) . Robinson, Alan JA; Voronkov, Andrei (編). Handbook of Automated Reasoning . Vol.  2. Elsevier. pp.  1149–. ISBN 978-0-444-50812-62007年7月27日にオリジナル（PDF）からアーカイブされました。
• Pfenning, Fr​​ank . 「17. 論理的枠組み」(PDF) .ハンドブック第2巻 2001年. pp. 1065–1148 . 
• Pfenning, Fr​​ank (1996). 「論理フレームワークの実践」. Kirchner, H. (編) 『代数とプログラミングにおける木構造 – CAAP '96』所収. Lecture Notes in Computer Science. Vol.  1059. Springer. pp. 119–134 . doi : 10.1007/3-540-61064-2_33 . ISBN  3-540-61064-2。
• コンスタブル、ロバート・L. (1998). 「X. コンピュータ科学、哲学、論理学における型」 . Buss, SR (編) 『証明論ハンドブック』 . 論理学研究シリーズ. 第 137巻. エルゼビア. pp. 683–786 . ISBN  978-0-08-053318-6。
• ヴィーダイク、フリーク (2005)。「世界の17の証明者」(PDF)。ラドボウド大学ナイメーヘン校。

• 定理証明器博物館
• 「依存型を用いた認定プログラミング入門」
• Coq証明支援システム入門（対話型定理証明の概要を含む）
• Agdaユーザー向け対話型定理証明
• 定理証明ツール一覧

カタログ

• カテゴリー別デジタル数学：戦術証明
• 自動控除システムとグループ
• 定理証明と自動推論システム
• 既存の機械化推論システムのデータベース
• NuPRL: その他のシステム
• 「特定の論理フレームワークと実装」 。 2022年4月10日にオリジナルからアーカイブ済み。2024年2月15日に取得。（フランク・フェニング著）
• DMOZ：科学：数学：論理と基礎：計算論理：論理的枠組み