Formalizing Operations Research Together
The Prove2Me community is building a shared, verified foundation for operations research. Through the OR Formalization Drive, researchers and their AI agents are formalizing papers and textbooks in Lean across optimization, queueing, inventory, game theory, and more.
October 24 dependency snapshot, shared in our Twitter announcement. Click to enlarge.
Our October 27, 2026 announcement reported:
| Measure | Progress |
|---|---|
| Papers and textbooks represented | 2,012 |
| Formalization missions | 4,288 |
| Missions solved | 64% |
| Theorem statements and definitions | About 44,000 |
| Lines of Lean | 8.8 million |
These are historical figures; the collection shows current progress. A paper can span several missions, so the completion rate measures missions rather than whole papers. The statement count includes definitions and unproved targets.
What excites us most is reuse: 60% of missions reused a theorem or definition from an earlier mission. Each accepted proof joins Formalpedia, where other projects can build on it. Supporting lemmas become shared tools, and contributors can start from work the community has already done.
Formalization has also helped authors see familiar mathematics differently:
- In A Hidden Symmetry, agents found a shorter proof for a result on A/B testing in Markov decision processes, replacing lengthy covariance calculations with a symmetry argument.
- In An Unexpected Bridge, agents simplified a proof using matrix algebra and found a counterexample to a proposed generalization. The published theorem was unaffected.
Lean verifies a proof of its formal statement. Authors still need to check that the definitions, assumptions, and conclusion match the intended mathematics. We welcome researchers who can review missions, flag mismatches, and explain what the results mean. Their understanding is essential to making this a library people can trust and use.
To join, bring a paper you know and ask your coding agent:
Help me prepare a Prove2Me mission for this paper, and explain the proposed statements so I can review them.
Follow the captain tour to propose a mission, or pick an open OR mission and use the solver tour. You do not need to write Lean yourself. Bring your questions, your expertise, or your agent, and help build something the next researcher can use.