The OR Formalization Drive
Help us formalize the operations research literature in Lean.
Collections
Curated groups of missions around a topic, textbook, or research area. Most open missions first.
20 collections
Famous Open Problems
Named conjectures and open problems with a precise Lean statement, from Riemann and Goldbach to Collatz and the Jacobian conjecture.
Queueing and Stochastic Networks
Single-server queues, Jackson and loss networks, heavy-traffic limits, fluid stability, and the control of queueing systems.
Scheduling Theory
Machine, flowshop, jobshop and project scheduling: optimality of classic rules, complexity reductions, and approximation guarantees.
Inventory and Supply Chain
Newsvendor and base-stock models, (s, S) policies, multi-echelon systems, and supply chain contracts.
Robust Optimization
Robust counterparts, uncertainty sets, adaptive policies, and distributionally robust optimization.
Revenue Management and Choice Models
Dynamic pricing, assortment optimization, discrete choice models, and airline seat control.
Online Algorithms
Competitive analysis: paging, k-server, metrical task systems, online primal-dual, secretary problems, and online matching.
Convex Polytopes
Grünbaum's Convex Polytopes: convex representations, face lattices, facet growth, and reconstruction from partial data.
High-Dimensional Probability and Statistics
Vershynin's High-Dimensional Probability and Wainwright's High-Dimensional Statistics: concentration, random matrices, and sparse recovery.
Erdős Problems
Problems from the Erdős problem list, each formalized as its own mission. Settle one, or decompose it into lemmas.
Discrete Convex Analysis
Murota's Discrete Convex Analysis, chapter by chapter: L-convex and M-convex functions, conjugacy, duality, and discrete separation.
Markov Decision Processes
Bäuerle and Rieder's Markov Decision Processes with Applications to Finance: Bellman equations, optimal policies, partial observation, and optimal stopping.
Convex Optimization
Convex optimization textbooks, chapter by chapter: KKT conditions, conic duality, barrier methods, and the complexity of first-order methods from center of gravity to mirror descent.
NP-Complete
A collection of NP-Complete problems as well as helpers.
OAI Math
All of openAI's results.
Introduction to Linear Optimization
Bertsimas and Tsitsiklis's Introduction to Linear Optimization: polyhedra, the simplex method, duality, and the ellipsoid method.
Bandit Algorithms
Lattimore and Szepesvári's Bandit Algorithms: regret bounds for explore-then-commit, UCB, Thompson sampling, and adversarial bandits.
Understanding Machine Learning
Shalev-Shwartz and Ben-David's Understanding Machine Learning: PAC learning, VC dimension, and the fundamental theorem of statistical learning.
Markov Chains and Mixing Times
Levin, Peres and Wilmer's Markov Chains and Mixing Times: coupling, spectral methods, and bounds on mixing.