[isabelle-dev] Sum_of_powers

Lawrence Paulson lp15 at cam.ac.uk
Mon Aug 15 15:31:50 CEST 2022

I think that HOL/ex/Sum_of_Powers.thy should be moved to the AFP.

It is a significant result: that the sum of the K-th powers of the first N positive integers is a polynomial in N. Using Bernoulli numbers and Bernoulli polynomials. This should not be hidden away in HOL-ex


More information about the isabelle-dev mailing list