論文の概要: Gödel's and Scott's Variants of the Ontological Argument in Lean 4
- arxiv url: http://arxiv.org/abs/2609.26806v1
- Date: Mon, 14 Sep 2026 17:10:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-25 00:05:17.681083
- Title: Gödel's and Scott's Variants of the Ontological Argument in Lean 4
- Title（参考訳）: Gödel's and Scott's Variants of the Ontological Argument in Lean 4
- Abstract要約: ポートは30個のLean 4加群で構成され、1つはIsabelle/HOL理論に従って、セクション構造、宣言順序、全ての公理、定義、補題、定理の名前を保持する。
イザベル/HOLの開発が証明した全てのことは、グデルの1970年の公理の不整合を含む、再び証明される。
- 参考スコア（独自算出の注目度）: 0.10152838128195468
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper presents a complete, structure-preserving port to Lean 4 of the Isabelle/HOL dataset accompanying Benzmüller and Scott's study of Gödel's modal ontological argument and Scott's variant of it. The port comprises 30 Lean 4 modules, one per Isabelle/HOL theory, retaining the section structure, the declaration order and the name of every axiom, definition, lemma and theorem; a comparison tool certifies all 548 statements identical. Everything the Isabelle/HOL development proves is proved again, including the inconsistency of Gödel's 1970 axioms, the repaired Gödel variants, Scott's variant, modal collapse, monotheism and the ultrafilter property of the positive properties; five statements the original leaves unreplayed after an automated prover had found a proof, one of which it then postulates, are proved as well. The 45 remaining unproved statements are exactly those the original refutes by nitpick (35) or leaves open (10); they are anonymous sorrys on which nothing depends. Two features of Lean 4 shape the result. It has neither a sledgehammer nor a model finder, so the one-line automated proofs become explicit proof terms and the 72 nitpick invocations are recorded as documentation. And #print axioms reports the postulates each proof consumes, giving for every result an upper bound on the modal logic it requires: Scott's necessary-existence theorem and modal collapse need only symmetry of the accessibility relation (logic KB); the essence and monotheism lemmas and the possible existence of a God-like being need no frame condition (the latter with the one exception the original records, the mixed-quantifier setting); and the inconsistency of Gödel's 1970 axioms needs none either. The development depends on no library beyond Lean 4's core; sources, comparison tools and two Isabelle cross-check sessions are included as ancillary files.
- Abstract（参考訳）: 本稿では、ベンツミュラーとスコットのゲーデルのモーダルな存在論とスコットの変種に関する研究を伴って、Isabelle/HOLデータセットのLean 4への完全な構造保存ポートを示す。
ポートは30のLean 4加群で構成され、1つのIsabelle/HOL理論はセクション構造、宣言順序、全ての公理、定義、補題、定理の名前を保持する。
ゲーデルの1970年の公理の不整合、修復されたゲーデルの変種、スコットの変種、モダル崩壊、モノシズム、そして正の性質の超フィルター性など、イザベル/HOLの開発が証明した全てのことが再び証明される。
残されている45の未証明の声明は、まさにニッチ(35)またはオープン(10)による元の反論である。
Lean 4の2つの特徴が結果を形作っています。
ハンマーもモデルファインダーも持っていないため、一行の自動証明は明示的な証明用語となり、72ニトピックの呼び出しは文書として記録されている。
スコットの必要存在定理とモジュラー崩壊は、アクセシビリティ関係の対称性のみを必要とする(論理KB)、本質と単神論の補題と神のような存在はフレーム条件を必要としない(後者は原記録と混合量子化器の設定がある)、そしてゲーデルの1970年の公理の不整合性はどちらも必要ではない。
ソース、比較ツール、および2つのIsabelleクロスチェックセッションは、補助ファイルとして含まれている。
関連論文リスト
- Reasoning Shortcuts and Value Symmetries: What Symmetry Permits, Architecture Realizes, and Optimization Selects [10.012788934490084]
推論ショートカット(Reasoning shortcuts)は、意図しない概念を通じて正しい予測を生成するニューロシンボリックシステムの規則の解である。
竹村、井上、西野の最近のフレームワークは、値を許容する自己同型群を通してそれらを分析している。
まず, 評価した4つのベンチマークのどれにも記載されているように, フレームワークの主要な定義である共有置換が適用されないことを示す。
論文 参考訳（メタデータ） (2026-08-11T03:10:20Z) - Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study [0.20415910628419062]
大規模言語モデル(LLM)は数学的証明に類似したテキストを生成することができるが、類似性は正確性を確立しない。
Coqのルールは、システムのどの証明ステップが受け入れられるかを定義する論理的フレームワークであるCalculus of Inductive Constructionsに基づいている。
このパイロット研究は、実際のCoqプロジェクトから派生したベンチマークであるCoqStoqから、同じ100の定理で6つのオープンウェイトLSMを評価した。
論文 参考訳（メタデータ） (2026-08-05T21:29:12Z) - Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
大規模言語モデル(LLM)は、自動的に証明を生成することを約束するが、既存のアプローチは、固定された人間設計の証明戦略をシステムに結び付ける。
このような戦略を課すことは不要で制限的であることを示す。
レムマ全体を一般的なコードエージェントに手渡して、独自のアプローチを自由に選択し、検証ハーネスにラップすることは、シンプルでより効果的です。
論文 参考訳（メタデータ） (2026-07-07T14:39:59Z) - ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。
ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。
実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
論文 参考訳（メタデータ） (2026-06-09T06:50:15Z) - Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement [69.77146194380488]
私たちはGoedel-Architectを紹介します。これは、青写真の生成と洗練に焦点を当てたLean 4で証明された公式な定理のためのフレームワークです。
Goedel-ArchitectがMiniF2Fテストで99.2%パス@1、PutnamBenchで75.6%パス@1を達成した。
これは、同等のオープンソースパイプラインよりも500倍低い価格で、オープンソースパイプラインの最先端のパフォーマンスを示している。
論文 参考訳（メタデータ） (2026-06-04T17:54:44Z) - LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
システムはマドリブの27の上位領域の戦術的利用分布を抽出する。
zスコアを計算して、ソースエリアで多用されるが、ターゲットエリアで稀または欠落している戦術を特定する。
これは、GPUアクセラレーションされたNPハードアナログを用いて、ソースとターゲットの証明状態と一致する。
論文 参考訳（メタデータ） (2026-04-19T03:27:16Z) - Mathematics with large language models as provers and verifiers [1.1029146548022293]
ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数理論の予想の約3分の1を閉じる。
論文 参考訳（メタデータ） (2025-10-11T20:35:25Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。
この合成データセットでDeepSeekMath 7Bモデルを微調整します。
我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文 参考訳（メタデータ） (2024-05-23T09:03:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。