Draft: Prototype of CVXPY to CvxLean converter#43

Open

SteveDiamond wants to merge 13 commits into

verified-optimization:mainfrom

SteveDiamond:main

Commits on Jul 24, 2025

feat: add CVXPY to CVXLean integration tools
SteveDiamond
committed
feat: complete working CVXPY to CVXLean integration with Mosek solver
SteveDiamond
committed
Clean up CVXPY integration: remove old code and rename working versions

SteveDiamond
and
claude
committed
Fix Portfolio.lean vector operations and improve CVXPY vector handling

SteveDiamond
and
claude
committed
Fix Portfolio.lean summation syntax and imports

SteveDiamond
and
claude
committed
Fix Portfolio.lean - now works perfectly with Mosek solver\!

SteveDiamond
and
claude
committed
Final fix: Add type annotations for Vec.sum objectives

SteveDiamond
and
claude
committed
remove integration status
SteveDiamond
committed
clean up MR
SteveDiamond
committed
Fix maximize objective support and Quadratic.lean type annotation

SteveDiamond
and
claude
committed
Add comprehensive logging and fix negative exponent syntax

SteveDiamond
and
claude
committed
Add support for ≥ (greater than or equal) constraints

SteveDiamond
and
claude
committed
Improve CVXPY to CvxLean conversion with log-sum-exp and reshape handling

SteveDiamond
and
claude
committed