## 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.