### Abstract

This article provides a formalisation of the symmetric
multivariate polynomials known as *power sum
polynomials*. These are of the form
p_{n}(*X*_{1},…,
*X*_{k}) =
*X*_{1}^{n}
+ … +
X_{k}^{n}.
A formal proof of the Girardâ€“Newton Theorem is also given. This
theorem relates the power sum polynomials to the elementary symmetric
polynomials s_{k} in the form
of a recurrence relation
(-1)^{k}
*k* s_{k}
=
∑_{i∈[0,k)}
(-1)^{i} s_{i}
p_{k-i} .

As an application, this is then used to solve a generalised
form of a puzzle given as an exercise in Dummit and Foote's
*Abstract Algebra*: For *k*
complex unknowns *x*_{1},
…,
*x*_{k},
define p_{j} :=
*x*_{1}^{j}
+ … +
*x*_{k}^{j}.
Then for each vector *a* ∈
ℂ^{k}, show that
there is exactly one solution to the system p_{1}
= a_{1}, …,
p_{k} =
a_{k} up to permutation of
the
*x*_{i}
and determine the value of
p_{i} for
i>k.