# State of DCP (Disciplined Convex Programming)

**URL:** <https://discourse.julialang.org/t/state-of-dcp-disciplined-convex-programming/131743>\
**Category:** Optimization (Mathematical)\
**Tags:** jump, disciplined-convex-p\
**Created:** [August 20, 2025, 9:25pm UTC](https://discourse.julialang.org/t/state-of-dcp-disciplined-convex-programming/131743 "2025-08-20T21:25:08Z")\
**Posts on this page:** 1\
**Showing post:** 15

<div class="post-metadata">

**Author:** ![langestefan](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/langestefan/32/207923_2.png) [@langestefan](https://discourse.julialang.org/u/langestefan)\
**Post date:** [August 25, 2025, 7:38pm UTC](https://discourse.julialang.org/t/state-of-dcp-disciplined-convex-programming/131743/15 "2025-08-25T19:38:01Z")

</div>

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](https://homepages.inf.ed.ac.uk/pbj/papers/iccopt25.pdf)

There’s a talk and a demo here: [Lean Together 2024: Ramon Fernández Mir, CvxLean, modeling convex optimization problems in Lean](https://www.youtube.com/watch?v=GNOXmt5A_MQ)

See also the [PhD thesis of Ramon](https://era.ed.ac.uk/bitstream/handle/1842/42057/Fern%C3%A1ndez%20Mir2024.pdf?sequence=1).

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 😃

---

_[View the full topic](https://discourse.julialang.org/t/state-of-dcp-disciplined-convex-programming/131743)._