Unity: A Multi-Agent Autoformalization Harness for Lean 4
Shivansh Gour, Riyaz Ahuja, Jeremy Avigad, Sean Welleck · GitHub
leanmulti-agentautoformalizationtheorem provingformal methods
- Developing a multi-agent autoformalization harness for Lean 4 designed to scale ensembles of smaller, less expensive models to frontier-level performance and use frontier models to push performance further.
- Designed a proof-orchestration architecture that mechanically extracts unresolved declarations and kernel dependencies into a dependency DAG, coordinates heterogeneous LLM agents in isolated Git worktrees, and automatically validates and merges candidate proofs.
- Built Lean-integrated agent infrastructure with LSP tooling, shared proof-search communication, concurrent strategy exploration, iterative critic loops, and persistent cross-run knowledge.
- Currently benchmarking Unity on FormalQualBench, where it has achieved state-of-the-art performance by solving 9 of the first 10 problems; on all 8 shared solves with the previous state of the art, reduced both cost and wall-clock time using cheaper, open-source models.
- presented at the hoskinson center for formal mathematics and at the l3 lab
- part of carnegie mellon university’s summer undergraduate research grant (surg)
Union: Efficient Decentralized Multi-Agent Coordination
Shivansh Gour
multi-agent
- Developing a general-purpose multi-agent harness that allows agents to self-organize around diverse problems and communicate efficiently while collaborating on large projects.
- Developing an online learning algorithm that adapts how agents are organized for each task using their trajectories over time, capabilities, and the evolving decomposition of the task.
- Built an end-to-end prototype supporting agent definition, spawning, execution, and inter-agent communication, with adapters for heterogeneous model providers and coding-agent harnesses.
Agora: Market-Based Multi-Agent Automated Mathematical Discovery
Riyaz Ahuja, Alexander Heckett, Shivansh Gour, Alexander Willoughby, Tate Rowney, Ishin Shah, Chris Su
leanmulti-agenttheorem provinggame theory
- Developing a multi-agent framework for automated mathematical discovery in which agents prove, conjecture, query, and exchange mathematical results through explicit economic mechanisms.
- Built experimental environments representing mathematics as dependency graphs, together with graph-transformer agents trained using reinforcement learning and infrastructure for automated search over collaboration mechanisms.
- Evaluating the framework on formal mathematics in Lean.
Market-Mediated Multi-Agent Theorem Proving in Lean 4
Riyaz Ahuja, Shivansh Gour · Advised by Fei Fang · report
leanmulti-agenttheorem provinggame theory
we model multi-agent theorem proving as an allocation problem over interdependent proof obligations. credit-only rewards can produce unbounded inefficiency; fully collateralized markets for proof-resolution events recover a bounded price of anarchy under sufficient liquidity, resolvability, and positive gains from trade. combining population-based reinforcement learning with these markets improves target resolution in synthetic games and raises proof completion from 34% to 52% on a lean 4 prime number theorem benchmark, while reducing duplicated work from 21% to 8%.
PraLean: Probabilistic Programming in Lean 4
Shivansh Gour, Riyaz Ahuja · Advised by Jan Hoffmann and Feras Saad
leanformal methods
- Developing a probabilistic programming library for Lean that supports executing arbitrary probabilistic programs while simultaneously proving their distributional correctness.
- Built a library of common probability distributions and a tactic that automatically proves distributional correctness for user-defined inference algorithms.
- Formalizes and verifies nontrivial sampling algorithms, including rejection sampling and Vitter’s reservoir sampling, proving that their operational implementations induce the intended distributions.
HoTTLean: Autoformalization for Homotopy Type Theory
HoTTLean Organization · Advised by Steve Awodey · GitHub
leanmulti-agentautoformalizationtheorem proving
- Developing autoformalization methods for HoTTLean, a Lean formalization of the groupoid model of homotopy type theory and the categorical semantics of Martin-Löf type theories.
- Applying multi-agent proof search to translate informal mathematical results into kernel-checked Lean formalizations and expand the project’s formal library.
