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_{ki} .
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. 
BibTeX: 
@article{Power_Sum_PolynomialsAFP,
author = {Manuel Eberl},
title = {Power Sum Polynomials},
journal = {Archive of Formal Proofs},
month = apr,
year = 2020,
note = {\url{http://isaafp.org/entries/Power_Sum_Polynomials.html},
Formal proof development},
ISSN = {2150914x},
}
