Back to AI Research

AI Research

Prove2Me: An Open Collaborative Platform for Scalin... | AI Research

Key Takeaways

  • Prove2Me is an open-source platform designed to scale the formalization of mathematics by enabling humans and AI agents to collaborate on Lean 4 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 ( this https URL ), an open collaborative platform for formalizing mathematics.
  • Users launch formalization "missions", to which AI agents contribute formal proofs toward completion.
Paper AbstractExpand

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 ( this https URL ), 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.

Prove2Me is an open-source platform designed to scale the formalization of mathematics by enabling humans and AI agents to collaborate on Lean 4 proofs. The platform aims to overcome the high barriers to entry in formal verification—such as the need for specialized expertise and the significant time required for manual proof writing—by allowing anyone with an AI agent to contribute to complex mathematical projects.

Mission-Based Formalization

To ensure the reliability of agent-generated content, Prove2Me uses a "mission" structure. A human captain defines a mission by selecting a headline goal, necessary definitions, and milestone lemmas. Humans audit this core set of statements to ensure they accurately represent the intended mathematics. Once the core is established, AI agents are free to generate intermediate theorems and proofs to complete the mission. This design limits the human audit surface while allowing for large-scale, automated proof generation.

Proof-Sketches and Decomposition

The platform uses "proof-sketches" to break down complex mathematical problems into smaller, manageable tasks. A proof-sketch is a Lean proof that relies on imported theorems or lemmas, even if those dependencies have not yet been proven. Because Prove2Me treats theorems and proofs as separate, immutable objects, agents can build on each other's work by importing existing results. This modularity allows a difficult theorem to be decomposed into atomized sub-problems, which can then be solved independently by different agents.

Verification and Auditing

Prove2Me employs a sub-agent read-back mechanism to make auditing accessible to non-experts. An auditor agent translates Lean code back into natural language LaTeX, allowing human auditors to verify that the formal statement matches the intended mathematical claim without needing to read Lean code directly. Once a proof is submitted, the platform uses the Lean 4 kernel to verify that the proof term matches the target statement. If a proof is accepted, it becomes a permanent, citable building block for future missions.

Addressing Scaling Obstacles

The authors identify three primary limitations in current formalization efforts that Prove2Me seeks to address:

  • Auditing: The difficulty of ensuring AI-generated proofs are not just technically correct in Lean, but also semantically faithful to the original problem.

  • Reusability: The tendency for existing formalizations to exist as monolithic, interdependent Git repositories that are difficult to integrate or reuse.

  • Scale: The reliance on single-organization compute resources, which limits the ability of the broader community to contribute to large-scale projects.
    By providing a platform where proofs are atomized and reusable, Prove2Me aims to transition math formalization from a centralized, expert-led activity into a scalable, crowd-sourced effort.

Comments (0)

No comments yet

Be the first to share your thoughts!