Back in February, I was talking with my PhD advisor about using Lean to formally verify automated optimization modeling outputs. It eventually turned into this paper [1]. It’s been truly incredible to see how much the frontier models have progressed in both autoformalization and automated theorem proving in the last six months. Back in February, it was cool to see them prove the validity of some simple cutting planes. Now it can churn out a min-cut max-flow duality formalization (not to mention FLT). Very exciting times!

I’ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2].

[1] https://arxiv.org/abs/2608.25220

[2] https://github.com/henryrobbins/open-atp