From acf9bcbb8d0e444f56d400bd71c9410314d0e61b Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Sat, 16 Mar 2024 20:05:30 +0000 Subject: [PATCH] doc: better phrasing in `README.md` --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index fc0f2f03..a9a05fba 100644 --- a/README.md +++ b/README.md @@ -5,8 +5,8 @@ CvxLean is a convex optimization modeling framework written in [Lean 4](https:// Problems are stated using definitions from [mathlib](https://github.com/leanprover-community/mathlib) and can be rigorously transformed both automatically and interactively. They can be solved by calling the backend solver [MOSEK](https://www.mosek.com/). Summary of features: -* **Formal definitions**. We define [minimization problems](https://verified-optimization.github.io/CvxLean/CvxLean/Lib/Minimization.html) and custom syntax allows users to define optimization problems in a natural way. We also define [equivalences](https://verified-optimization.github.io/CvxLean/CvxLean/Lib/Equivalence.html), [reductions](https://verified-optimization.github.io/CvxLean/CvxLean/Lib/Reduction.html), and [relaxations](https://verified-optimization.github.io/CvxLean/CvxLean/Lib/Relaxation.html). -* **User-guided transformations**. For each relation (equivalence, reduction, and relaxation), we have formalized several transformations that preserve the corresponding relation. These are realized as tactics and can be applied interactively in the `equivalence`, `reduction`, or `relaxation` commands. +* **Formal definitions**. Users can define [optimization problems](https://verified-optimization.github.io/CvxLean/CvxLean/Lib/Minimization.html) in a natural way using custom syntax. These are formal objects we can reason about; usually, we want to talk about [equivalences](https://verified-optimization.github.io/CvxLean/CvxLean/Lib/Equivalence.html), [reductions](https://verified-optimization.github.io/CvxLean/CvxLean/Lib/Reduction.html), and [relaxations](https://verified-optimization.github.io/CvxLean/CvxLean/Lib/Relaxation.html). +* **User-guided transformations**. For each relation (equivalence, reduction, and relaxation), we have formalized several relation-preserving transformations. These are realized as tactics and can be applied interactively in the `equivalence`, `reduction`, or `relaxation` commands. * **Proof-producing DCP transformation**. Our main contribution is a verified version of the [disciplined convex programming (DCP)](https://web.stanford.edu/~boyd/papers/disc_cvx_prog.html) canonization algorithm. It can be used through the `dcp` tactic. The `solve` command also uses it behind the scenes. * **Automatic transformation into DCP form**. The `pre_dcp` tactic uses [egg](https://github.com/egraphs-good/egg) to find a sequence of rewrites to turn a problem into an equivalent DCP-compliant problem.