Isabelle/HOL is an open-source interactive theorem prover. The version used for this formalization is Isabelle2022 (as of writing this the most recent version).
This formalization follows the original paper:
A. Kate, G. Zaverucha, and I. Goldberg. Polynomial commitments. Technical report, 2010. CACR 2010-10, Centre for Applied Cryptographic Research, University
of Waterloo
First step is to prove the DL version.
Correctness i.e. the interaction between an honest prover and an honest verifier, yields a correct result.
The security properties are the same as in the paper. They are shown via game-based proofs, see the CryptHOL tutorial for details.
(thanks to Katharina Kreuzer for providing the Elimination of repeated factors (ERF) algorithm, which allowed a complete factorization)
Though this property is not explicitly stated in the original paper, it is commonly referred to and needed for zk-SNARK protocols, such as PLONK and Sonic.