論文の概要: 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?

• arxiv url: http://arxiv.org/abs/2601.03298v1
• Date: Tue, 06 Jan 2026 01:01:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-09 02:15:22.971625
• Title: 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?
• Title（参考訳）: 2週間で130k行の形式的トポロジ: シンプルでチープなオートフォーマライゼーション?
• Authors: Josef Urban,
• Abstract要約: このプロジェクトは2025年11月21日から実行され、2026年1月4日現在160万行の形式化されたトポロジーを生産している。 ほとんど(約130kの路線)は12月22日から1月4日までの2週間で、LCMのサブスクリプション料金は約100ドルである。
• 参考スコア（独自算出の注目度）: 1.827510863075184
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This is a brief description of a project that has already autoformalized a large portion of the general topology from the Munkres textbook (which has in total 241 pages in 7 chapters and 39 sections). The project has been running since November 21, 2025 and has as of January 4, 2026, produced 160k lines of formalized topology. Most of it (about 130k lines) have been done in two weeks,from December 22 to January 4, for an LLM subscription cost of about \$100. This includes a 3k-line proof of Urysohn's lemma, a 2k-line proof of Urysohn's Metrization theorem, over 10k-line proof of the Tietze extension theorem, and many more (in total over 1.5k lemmas/theorems). The approach is quite simple and cheap: build a long-running feedback loop between an LLM and a reasonably fast proof checker equipped with a core foundational library. The LLM is now instantiated as ChatGPT (mostly 5.2) or Claude Sonnet (4.5) run through the respective Codex or Claude Code command line interfaces. The proof checker is Chad Brown's higher-order set theory system Megalodon, and the core library is Brown's formalization of basic set theory and surreal numbers (including reals, etc). The rest is some prompt engineering and technical choices which we describe here. Based on the fast progress, low cost, virtually unknown ITP/library, and the simple setup available to everyone, we believe that (auto)formalization may become quite easy and ubiquitous in 2026, regardless of which proof assistant is used.
• Abstract（参考訳）: これは、Munkresの教科書(全241ページ、7章、39節)から、既に一般的なトポロジの大部分を自己形式化したプロジェクトの簡単な記述である。 このプロジェクトは2025年11月21日から実行され、2026年1月4日現在160万行の形式化されたトポロジーを生産している。 ほとんど(約130kの路線)は12月22日から1月4日までの2週間で、LCMのサブスクリプション費用は約100ドルである。 これには、ウルソンの補題の3k線証明、ウルソンのメートル化定理の2k線証明、ティーツェ拡張定理の10k線証明、さらに多くのものが含まれている(合計1.5kの補題/定理)。 LLMとコアとなる基礎ライブラリを備えた合理的に高速な証明チェッカーとの間に長期にわたるフィードバックループを構築する。 LLM は ChatGPT (主に 5.2) または Claude Sonnet (4.5) としてインスタンス化され、それぞれの Codex または Claude Code コマンドラインインターフェースを介して実行される。 証明チェッカーはチャド・ブラウンの高階集合論体系 Megalodon であり、コアライブラリはブラウンの基本的な集合論と超現実数(実数など)の形式化である。 残りは、ここで説明するような、迅速なエンジニアリングと技術的な選択です。 高速な進歩、低コスト、事実上未知のIPP/ライブラリ、そして誰もが利用できる単純なセットアップに基づいて、2026年には(オート)フォーマル化は、どの証明アシスタントが使われているかに関わらず、非常に簡単でユビキタスになると信じている。

関連論文リスト

• 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)
• Polybasic Speculative Decoding Through a Theoretical Perspective [68.71678077009386]
  推論レイテンシは、大規模言語モデルの大規模展開において重要なボトルネックである。 本稿では,包括的理論的解析を基盤とした,新しいエンポリベーシックな投機的復号化フレームワークを提案する。 我々の手法は、LLaMA2-Chat 7Bの3.31times$から4.01times$、LLaMA3-8Bの3.87倍、Vicuna-7Bの4.43倍、Qwen2-7Bの3.85倍の3.85倍のスピードアップ比が得られることを示す。
  論文  参考訳（メタデータ） (2025-10-30T14:20:24Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。 それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
  論文  参考訳（メタデータ） (2025-05-20T05:15:47Z)
• 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)
• A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems [0.0]
  リーンの残りのIMO問題に対する完全な、オリジナルの公式な証明を書いています。 この取り組みは,5,880行のリーン証明を作成することで,現在パブリックドメインにある証明の可用性を拡大するものだ。
  論文  参考訳（メタデータ） (2024-11-28T02:50:42Z)
• REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
  我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。 新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。 また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
  論文  参考訳（メタデータ） (2024-02-26T21:21:30Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。 コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。 新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
  論文  参考訳（メタデータ） (2022-11-14T16:52:32Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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