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.


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.