doc: better phrasing in README.md

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.