論文の概要: Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

• arxiv url: http://arxiv.org/abs/2605.20120v1
• Date: Tue, 19 May 2026 17:08:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-20 15:03:09.546333
• Title: Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
• Title（参考訳）: リーン4のAI支援理論証明にAristotle APIを使用する: グラスホッパー問題の形式化ケーススタディ
• Authors: Gabriel Rongyang Lau,
• Abstract要約: 本稿では,この問題に対するAristotle API証明の試みをLean 4形式化したケーススタディについて報告する。 生成されたアーティファクトは、定理の一般化されたリーンバージョンを記述し、最大性と隣接するスワップ交換戦略の局所的な構成要素に対する検証済みのヘルパー補題を4つ含んでいる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI-assisted theorem proving can now generate substantial Lean developments for olympiad-level mathematics, but the evidential status of such developments depends on which declarations are actually verified. This paper reports a Lean 4 formalization case study of an Aristotle API proof attempt for the Grasshopper problem, originally posed as IMO 2009 Problem 6. The generated artifact states a generalized Lean version of the theorem, contains four verified helper lemmas for local components of a maximality and adjacent-swap exchange strategy, and leaves the main theorem grasshopper closed directly by one unresolved sorry. The verified components establish that the final partial sum equals the total sum, that an adjacent transposition can affect only the relevant intermediate partial sum, that the changed partial sum has the expected form, and that maximality at a position admitting an adjacent successor swap forces a corresponding forbidden-set membership fact. The Aristotle output summary identifies the intended remaining mathematical step as the global counting step needed to show that these membership facts produce at least n distinct forbidden values, contradicting the cardinality assumption |M| < n; the Lean source itself does not reduce the main theorem to a separately encoded counting lemma. This case study gives an inspectable example of a central limitation in AI-assisted formalization, namely that local proof search can succeed while the global combinatorial bookkeeping required for a theorem remains unresolved. The paper contributes a reproducible Lean artifact and a precise analysis of its verified and unverified proof content.
• Abstract（参考訳）: AIによる定理証明は、今やオリンピックレベルの数学のための実質的なリーン開発を生み出すことができるが、そのような発展の明らかな状態は、どの宣言が実際に検証されているかによって異なる。 本稿では,当初IMO 2009 Issue 6として提案されていたGrasshopper問題に対するAristotle API証明の試みについて,Lean 4のケーススタディを報告する。 生成されたアーティファクトは、定理の一般化されたリーンバージョンを記述し、最大性と隣接するスワップ交換戦略の局所成分に対する証明済みのヘルパー補題を4つ含み、未解決の許しにより、主定理のグラスホッパーを直接閉じる。 検証された成分は、最終部分和が総和と等しいこと、隣接する転置が関連する中間部分和のみに影響を与えること、変化した部分和が期待される形式を持つこと、および、隣接する後続スワップを許容する位置における最大性は、対応する禁止セットのメンバシップ事実を強制することを保証する。 アリストテレス・アウトプット・サマリー(英語版)は、意図された数学的ステップを、これらのメンバーシップの事実が少なくとも n 個の異なる禁じられた値を生成することを示すのに必要な大域的な数え上げステップとして定義し、濃度の仮定 |M| < n と矛盾する。 このケーススタディでは、AI支援形式化における中心的な制限の検査可能な例、すなわち、局所的な証明探索が成功し、定理に必要なグローバルな組合せ簿記が未解決のままであることを示す。 この論文は再現可能なリーンアーティファクトと、その検証済みかつ未検証の証明内容の正確な分析に貢献する。

関連論文リスト

• Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants [0.0]
  大規模言語モデルは、構造化論理的推論において体系的な制限を示す。 LLM支援推論のための明示的なプロトコルとして、パースの三部構造推論を運用するシンボリックな足場を提案する。
  論文  参考訳（メタデータ） (2026-04-17T05:59:16Z)
• Exact Structural Abstraction and Tractability Limits [0.0]
  正確な正確性は、誘導されたクラス $s sim_R simation' iff MathrmAdm_R(s)$ にのみ依存する。 決定、探索、近似、統計的、ランダム化された地平線、分布保証は全て同じ商-回復問題に還元される。
  論文  参考訳（メタデータ） (2026-04-08T17:59:47Z)
• PBLean: Pseudo-Boolean Proof Certificates for Lean 4 [27.126691338850254]
  PBLean は VeriPB pseudo-Boolean (PB) 証明証明書をLean 4 にインポートする手法である。 リーンで完全証明され、コンパイルされたネイティブコードとして実行されるブールチェッカー関数。 我々のチェッカーは、カットプレーンや証明・バイ・コントラディション・サブプロテクションを含む全てのVeriPBカーネルルールをサポートしている。
  論文  参考訳（メタデータ） (2026-02-09T14:13:30Z)
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
  大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。 しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。 機械学習の基礎理論に基づいて構築された、リーン4ベンチマークであるFormalMLを紹介します。
  論文  参考訳（メタデータ） (2025-09-26T14:40:14Z)
• CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
  我々は,系統的かつ包括的な推論プロセスを実行するためのモデルを導くことで,モデルがよりきめ細やかで正確な絞り込み決定を実行できることを提案する。 我々は,(i)クレームの分解,(ii)サブクレームの属性と包含分類,および(iii)集約分類から成る3段階の推論プロセスを定義し,そのような導出推論が実際に幻覚検出の改善をもたらすことを示す。
  論文  参考訳（メタデータ） (2025-06-05T17:02:52Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。