Symbolic summation methods and congruences involving harmonic numbers

In this paper, we establish some combinatorial identities involving harmonic numbers via the package Sigma , by which we confirm some conjectural congruences of Z.-W. Sun. For example, for any prime p > 3 , we have ∑ k = 0 ( p − 3 ) / 2 ( 2 k k ) 2 ( 2 k + 1 ) 16 k H k ( 2 ) ≡ − 7 B p − 3 ( mod p ) , ∑ k = 1 p − 1 ( 2 k k ) 2 k 16 k H 2 k ( 2 ) ≡ B p − 3 ( mod p ) , ∑ k = 1 ( p − 1 ) / 2