Low-cost AI agents for formal mathematics and verification

Formal proofs are becoming critical infrastructure, and they are expensive to maintain.

• Machine-checked proofs now underpin mathematics libraries such as Mathlib, verified cryptography, programming-language semantics and physics formalizations.
• Proofs written by people or by AI models are often long and slow to check, and they break when the proof assistant or its libraries are upgraded.
• Cleaning and porting them takes scarce expert time. Unchecked AI output cannot be trusted in this setting.

An agent that refactors Lean 4 proofs and proves every change with the compiler.

• Shorter proofs: fewer tokens for the same theorem, with the statement unchanged.
• Cheaper to check: fewer heartbeats, Lean's deterministic measure of checking work.
• Version-robust: the same proof compiles unchanged on every Lean version it is checked against (all listed versions in the Arena).
• Low cost by design: our competition agent runs under a fixed API budget per problem (US$3 in the closed track) and can also run on open-weight models on self-hosted GPUs.

#1 on the closed-source LLM track of the Lean Refactor Arena's public warm-up leaderboard.

As of October 20, 2026, on the 15 public warm-up problems (three each from Strata, PhysLib, CSLib, ArkLib and PutnamBench). The Arena is the competition of the AI for Verifiable Coding (VeriCodeGen) workshop at NeurIPS 2026; the full 50-problem benchmark opens November 1, when the leaderboard is refreshed, and final results are announced November 22. The warm-up board accepts any method: our 93.02 entry is a development portfolio built from many runs and is not limited to the track's US$3-per-problem budget. Final rankings come from the organizers' reproduction of the top entries' submitted code under that budget.

• Research: "The Verification Gap: Auditing Proof Progress and Repair on IMO 2026", accepted at the MATH-AI 2026 workshop at NeurIPS 2026.
• Autoresearch: two Kaggle silver medals in 26 days (NeuroGolf and ROGII) with one reusable research system.

Models propose; the compiler decides.

• An agent harness drives language models with the Lean compiler in the loop.
• Every candidate is compiled and measured for length, checking cost and compatibility before it is kept. Nothing is accepted on a model's word.
• Model calls are budgeted per problem.
• The same harness runs frontier API models or self-hosted open-weight models, so the cost can be chosen per task.

Code, reproduction steps and our technical report will be published after the competition: github.com/bobbercheng/vexorium-lean-refactor.

We start where answers can be verified, prove the method in public competitions, then sell the same agents to teams with domain problems of their own.

• November 2026: final runs on the Arena's full 50-problem benchmark; technical report and code release after the competition.
• December 2026: presenting the Verification Gap paper at the MATH-AI workshop, NeurIPS 2026.
• Next: pilots of the proof refactoring agent with teams that maintain Lean projects, and early access to the market research agent.

Co-founder: Bobber Cheng, author of the MATH-AI 2026 paper above.