Skip to content
Log in
Sponsored AI Networking Cookbook: Practical recipes for AI-assisted network automation and development AI Networking Cookbook: Practical recipes for AI-assisted network automation and development
#artificial intelligence Preprint

Prove2Me: An Open Collaborative Platform for Scaling Math Formalization

Shu-Ze Chen Kunal Marwaha Xiao-Yang Lu Henry S. Yuen Tianshu Peng
Aug 2026 · 0 citations · 33 references
Computer Science

TL;DR

Prove2Me aims to turn math formalization into a scalable, crowd-sourced effort open to anyone with an agent, and designed mechanisms and a specialized harness that enable large-scale collaboration so that agents can build on one another's work and freely reuse existing results.

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.

DOI arXiv Semantic Scholar
View source

Similar papers

#artificial intelligence Open access May 2023

Evaluating the Performance of Large Language Models on GAOKAO Benchmark

GAOKAO-Bench is introduced, an intuitive benchmark that employs questions from the Chinese GAOKAO examination as test samples, including both subjective and objective questions that contribute a robust evaluation benchmark for future large language models and offers valuable insights into the advantages and limitations of such models.

Xiaotian Zhang, Chun-yan Li, Yi Zong et al. · 216 citations · ⚡17
#artificial intelligence Open access Jul 2024

Gender, Race, and Intersectional Bias in Resume Screening via Language Model Retrieval

This work investigates the possibilities of using LLMs in a resume screening setting via a document retrieval framework that simulates job candidate selection and finds that the MTEs are biased, significantly favoring White-associated names in 85% of cases and female-associated names in only 11.1% of cases.

Kyra Wilson, Aylin Caliskan · 131 citations · ⚡8
#artificial intelligence Feb 2025

PRISM: Self-Pruning Intrinsic Selection Method for Training-Free Multimodal Data Selection

Empirically, PRISM reduces the end-to-end time for data selection and model tuning to just 30% of conventional pipelines, and achieves this efficiency while simultaneously enhancing performance, surpassing models fine-tuned on the full dataset across eight multimodal and three language understanding benchmarks.

Jinhe Bi, Yifan Wang, Danqi Yan et al. · 73 citations · ⚡4
#artificial intelligence Conference Open access Apr 2020

ECCOLA - a Method for Implementing Ethically Aligned AI Systems

The method, ECCOLA, is presented, which aims at making the high-level AI ethics principles more practical, making it possible for developers to more easily implement them in practice.

Ville Vakkuri, Kai-Kristian Kemell, P. Abrahamsson · 64 citations · ⚡6
#artificial intelligence May 2023

Let the Flows Tell: Solving Graph Combinatorial Optimization Problems with GFlowNets

This paper designs Markov decision processes (MDPs) for different combinatorial problems and proposes to train conditional GFlowNets to sample from the solution space and demonstrates that GFlowNet policies can efficiently find high-quality solutions.

Dinghuai Zhang, H. Dai, Esmeralda S. Whitammer et al. · 59 citations · ⚡8
#artificial intelligence Jun 2019

Ethically Aligned Design of Autonomous Systems: Industry viewpoint and an empirical study

An empirical study on the current state of practice in artificial intelligence ethics is conducted by means of a multiple case study of five case companies, which indicates a gap between research and practice in the area.

Ville Vakkuri, Kai-Kristian Kemell, Joni Kultanen et al. · 56 citations · ⚡6

Related blog posts

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.