Lean Formalization Agents for Mathematics in Operations Research Workshop

This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology. The participants in the workshop will work with the agent, end-to-end, starting from a PDF version of a paper, and then producing a report, containing a diagram describing the mathematical results and statements, an assessment of what results are rigorously verified, which ones are repairable, and which results are not repairable (by providing a counter-example) or potentially very difficult to repair. If the paper is verifiable or repairable, the agent also provides a Lean formalized version of the results.

Presenters: Guanting Chen, Xiaocheng Li, Shang Liu, and Jose Blanchet

Workshop Fee: $25

All workshop participants are required to register for the 2026 INFORMS Annual Meeting in San Francisco. The registration fee for this workshop does NOT include the registration fee for the INFORMS Annual Meeting.