  We give a proof of two identities involving binomial sums at infinity
conjectured by Z-W Sun. In order to prove these identities, we use a recently
presented method i.e. we view the series as specializations of generating
series and derive integral representations. Using substitutions, we express
these integral representations in terms of cyclotomic harmonic polylogarithms.
Finally, by applying known relations among the cyclotomic harmonic
polylogarithms, we derive the results. These methods are implemented in the
computer algebra package HarmonicSums.
