論文の概要: Prove2Me: An Open Collaborative Platform for Scaling Math Formalization

• arxiv url: http://arxiv.org/abs/2608.28433v2
• Date: Mon, 31 Aug 2026 13:30:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-01 15:47:04.433122
• Title: Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
• Title（参考訳）: Prove2Me: 数学の形式化をスケールするためのオープンなコラボレーションプラットフォーム
• Authors: Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng,
• Abstract要約: 数学の形式化のためのオープンな協調プラットフォームであるProve2Meを紹介する。 ユーザーは、AIエージェントが完了に向けた公式な証明に貢献する正式な「ミッション」を起動する。 Prove2Meは、数学の定式化を、エージェントのある人なら誰でも、スケーラブルでクラウドソースの努力にしたい、と願っている。
• 参考スコア（独自算出の注目度）: 5.249471979820288
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Proof assistants such as Lean 4 promise the paradigm of formally verified mathematics, but large-scale formalization projects have faced major barriers to entry, including the need for expertise in formal verification (as well as the underlying mathematics) and the significant time required for writing formal proofs. AI coding agents have dramatically reduced these barriers; human users can now use natural language to prompt agents to write complex proofs in Lean. This opens up the intriguing possibility of internet-scale mathematical collaboration involving both humans and AI agents, where correctness is machine-checked. To realize this possibility, we introduce Prove2Me (https://prove2.me), an open collaborative platform for formalizing mathematics. Users launch formalization "missions", to which AI agents contribute formal proofs toward completion. We designed mechanisms and a specialized harness in Prove2Me that enable large-scale collaboration so that agents can build on one another's work and freely reuse existing results. In doing so, Prove2Me aims to turn math formalization into a scalable, crowd-sourced effort open to anyone with an agent.
• Abstract（参考訳）: リーン4のような証明アシスタントは、正式に証明された数学のパラダイムを約束するが、大規模な形式化プロジェクトは、形式的な検証(基礎となる数学と同様に)の専門知識の必要性や、形式的な証明を書くのに必要なかなりの時間など、導入の大きな障壁に直面している。 AIコーディングエージェントは、これらの障壁を劇的に減らした。人間のユーザは自然言語を使って、エージェントにリーンで複雑な証明を書くように促すことができる。 これにより、人間とAIエージェントの両方が関与する、インターネット規模の数学的コラボレーションの興味深い可能性が開き、正しさがマシンチェックされる。 この可能性を実現するために,数学を形式化するオープンな協調プラットフォームであるProve2Me(https://prove2.me)を紹介した。 ユーザーは、AIエージェントが完了に向けた公式な証明に貢献する正式な「ミッション」を起動する。 Prove2Meのメカニズムと特殊なハーネスを設計し、エージェント同士の作業で大規模コラボレーションを可能にし、既存の結果を自由に再利用できるようにしました。 Prove2Meは、数学の定式化を、エージェントのある人なら誰でも、スケーラブルでクラウドソースの努力にしたい、と願っている。

関連論文リスト

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。 MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
  論文  参考訳（メタデータ） (2026-07-16T05:22:40Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。 最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。 汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-06-30T05:05:03Z)
• Characterizing initial human-AI proof formalization workflows [66.06866890889131]
  AIシステムのコード生成能力の進歩と、証明を形式化し、検証する人々の能力を変えるための高度な数学的推論の約束への関与。 我々は、AIが人々のフォーマル化に与える影響について、混合メソッド分析を行う。 質的な調査では、人々の好みは多様であるが、形式化におけるAI支援に対する一般的な欲求が示されている。
  論文  参考訳（メタデータ） (2026-06-02T22:58:19Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs [11.87831709160905]
  本稿では,自動定理証明のためのAIエージェントであるProver Agentを紹介する。 大規模な言語モデル(LLM)と公式な証明アシスタントであるLeanを統合している。 MiniF2Fベンチマークで88.1%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-06-24T18:01:52Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。 コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。 新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
  論文  参考訳（メタデータ） (2022-11-14T16:52:32Z)
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs [30.57062828812679]
  本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。 大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
  論文  参考訳（メタデータ） (2022-10-21T22:37:22Z)

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

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