State of DCP (Disciplined Convex Programming)

Specific Domains Optimization (Mathematical)
,
15

I came across some work on DCP implemented in Lean, a DCP/rewriting engine called CvxLean. Looks very interesting: CvxLean - a convex optimization modeling framework based on the Lean 4 proof assistant

There’s a talk and a demo here: Lean Together 2024: Ramon Fernández Mir, CvxLean, modeling convex optimization problems in Lean

See also the PhD thesis of Ramon.

I wonder if this could be used as common middleware layer between cvxpy/jump/? and a DCP representation. Everyone involved seems to be talking about the same things and has the same goals.

*just realized CvxLean was also referenced in the CVX forum post :smiley:

3 Likes