[isabelle-dev] Sum_of_powers

Manuel Eberl manuel at pruvisto.org
Mon Aug 15 15:53:15 CEST 2022

It already is in the AFP: 

If I recall correctly, I took Lukas's theory from HOL-ex, added a lot of 
my own stuff, and put it in the AFP (with his permission and with him as 
a co-author).

As for why I did not delete the version in HOL-ex, I cannot remember – 
perhaps because it still is a small and self-contained derivation of 
that result.


On 15/08/2022 15:31, Lawrence Paulson wrote:
> 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
> Larry
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list