Draft: Prototype of CVXPY to CvxLean converter

.gitignore

@@ -12,5 +12,6 @@
 /playground
 /scripts/evaluation/data
 /plots
+**/__pycache__/
 
 /CvxLean/Command/Solve/Mosek/Path.lean

CvxLean/Examples/CVXPY/Portfolio.lean

@@ -0,0 +1,22 @@
+import CvxLean
+
+noncomputable section
+
+open CvxLean Minimization Real BigOperators
+
+def portfolio_optimization :=
+  optimization (weights : Fin 3 → ℝ)
+    minimize (Vec.sum (weights ^ 2) : ℝ)
+    subject to
+      c1 : Vec.sum weights = 1
+      c2 : ∀ i, 0 ≤ weights i
+
+-- Solve the problem directly (applies pre_dcp automatically)
+solve portfolio_optimization
+
+-- Check the results
+#eval portfolio_optimization.status
+#eval portfolio_optimization.solution
+#eval portfolio_optimization.value
+
+end

CvxLean/Examples/CVXPY/Quadratic.lean

@@ -0,0 +1,22 @@
+import CvxLean
+
+noncomputable section
+
+open CvxLean Minimization Real BigOperators
+
+def quadratic_problem :=
+  optimization (x : ℝ)
+    minimize (x + (-1)) ^ 2
+    subject to
+      c1 : 0 ≤ x
+      c2 : x ≤ 2
+
+-- Solve the problem directly (applies pre_dcp automatically)
+solve quadratic_problem
+
+-- Check the results
+#eval quadratic_problem.status
+#eval quadratic_problem.solution
+#eval quadratic_problem.value
+
+end