論文の概要: Munkres' General Topology Autoformalized in Isabelle/HOL

• arxiv url: http://arxiv.org/abs/2604.07455v1
• Date: Wed, 08 Apr 2026 18:00:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-10 18:34:05.487475
• Title: Munkres' General Topology Autoformalized in Isabelle/HOL
• Title（参考訳）: Isabelle/HOLにおけるMunkresの一般的なトポロジー
• Authors: Dustin Bryant, Jonathan Julián Huerta y Munive, Cezary Kaliszyk, Josef Urban,
• Abstract要約: 我々は,85,000行以上のIsabelle/HOLコードを生成するLDM支援オートフォーマル化実験について述べる。 形式化は完備であり、806の形式的な結果はすべて、ゼロ・ノウハウで完全に証明される。 得られた形式化を詳細に分析し,セッションログから人間-LLM相互作用パターンを分析し,関連する自己形式化の取り組みと比較した。
• 参考スコア（独自算出の注目度）: 2.5899040911480182
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Chapters 2--8), from topological spaces through dimension theory. The LLM-based coding agents (initially ChatGPT 5.2 and then Claude Opus 4.6) used 24 active days for that. The formalization is complete: all 806 formal results are fully proved with zero sorry's. Proved results include the Tychonoff theorem, the Baire category theorem, the Nagata--Smirnov and Smirnov metrization theorems, the Stone--Čech compactification, Ascoli's theorem, the space-filling curve, and others. The methodology is based on a "sorry-first" declarative proof workflow combined with bulk use of sledgehammer - two of Isabelle major strengths. This leads to relatively fast autoformalization progress. We analyze the resulting formalization in detail, analyze the human--LLM interaction patterns from the session log, and briefly compare with related autoformalization efforts in Megalodon, HOL Light, and Naproche. The results indicate that LLM-assisted formalization of standard mathematical textbooks in Isabelle/HOL is quite feasible, cheap and fast, even if some human supervision is useful.
• Abstract（参考訳）: マンクルズトポロジ(一般トポロジ、章2-8)の39区間すべてをカバーする85,000行以上のIsabelle/HOL符号を,次元理論を通じて位相空間から生成するLLM支援自己形式化実験について述べる。 LLMベースのコーディングエージェント(最初はChatGPT 5.2、後にClaude Opus 4.6)は24日間を使用。 形式化は完備であり、806 の形式的な結果はすべて、ゼロ・ノウハウで完全に証明される。 証明された結果は、ティコノフの定理、ベール圏の定理、ナガタ=スミルノフとスミルノフの計量化の定理、ストーン=シェッヒのコンパクト化、アスコリの定理、空間充填曲線などである。 この方法論は、Isabelleの主要な強みの2つであるハンマーのバルク使用と合わせて、"sorry-first"宣言的証明ワークフローに基づいている。 これにより、比較的高速な自己形式化が進行する。 得られた形式化を詳細に分析し、セッションログから人-LLM相互作用パターンを分析し、Megalodon, HOL Light, Naprocheにおける関連する自己形式化の取り組みと比較した。 その結果,Isabelle/HOL における標準数学教科書の LLM 支援形式化は,人的監督が有用であっても,実現可能で,安価で,高速であることが示唆された。

関連論文リスト

• Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
  本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。 エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。 この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
  論文  参考訳（メタデータ） (2026-02-02T16:24:53Z)
• LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories) [7.871706113805829]
  LeanCatは、カテゴリ理論の形式化のためのリーンベンチマークである。 パート I: 1-カテゴリには、完全に形式化されたステートメントレベルのタスクが100個含まれています。 Part II: LeanBridgeはLeanExploreを使ってMathlibを検索し、単一モデルベースラインに対する一貫した利得を観察します。
  論文  参考訳（メタデータ） (2025-12-31T11:33:29Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving [53.43068330741449]
  大規模言語モデル(LLM)を用いた対話型形式検証環境FVELを提案する。 FVELは、検証対象のコードをIsabelleに変換し、LLMで証明された神経自動定理を用いて検証を行う。 FVELERデータセットには、Isabelleで定式化されたコード依存関係と検証プロセスが含まれており、758の理論、29,125のレムマ、200,646の証明ステップが含まれている。
  論文  参考訳（メタデータ） (2024-06-20T15:31:05Z)
• 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)

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

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