## Interesting Solved/Unsolved Conjectures.

- Conjecture $\frac{1}{n(n+2)}$: “
*For every even positive integer $n$, there exist polynomial sums of squares $\sigma_0, \sigma_1, \dots, \sigma_m \in \mathbb{R}_{n-2}[x]$ such that $\prod_{i=1}^n x_i + \frac{1}{n(n + 2)} = \sigma_0 + \sum_{i=1}^n \sigma_i \, x_i \, (1 - x_i)$*”. For more details, see the paper Error Bounds for Some Semidefinite Programming Approaches to Polynomial Minimization on the Hypercube, where the conjecture is stated by De Klerk and Laurent.

- Generalized Lax Conjecture: “
*Every hyperbolicity cone is spectrahedral*”. For more details, see the slides by Tim Netzer.

- Kepler Conjecture: “
*The maximal density of sphere packings in 3D-space is $\frac{\pi}{18}$*”.

The formal verification project of the conjecture was completed on August 10, 2014.

- Reformulation of Bessis-Moussa-Villani (BMV) Conjecture by Lieb and Seiringer: “
*For all positive semidefinite matrices $A$ and $B$ and all $m \in \mathbb{N}$, the single variable polynomial $p(t) := \mathop{Tr}((A + tB)^m)$ has only nonnegative coefficients*“. A proof of the conjecture by Herbert R Stahl is available here.

## Software.

### Program Verification:

- GPUVerify: a Verifier for GPU Kernels.
- Boogie: An Intermediate Verification Language.

### Semidefinite Programming:

- Mosek: a solver for various mathematical optimization problems.
- SDPT3: a MATLAB software for semidefinite-quadratic-linear programming.
- SDPA: Semidefinite Programming Algorithms.
- Yalmip: a MATLAB toolbox for advanced modeling and solution of convex and nonconvex optimization problems.