Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Polygonal_Number_Theorem

Email Gateway (Aug 11 2023 at 09:16):

From: Tobias Nipkow <nipkow@in.tum.de>
Polygonal_Number_Theorem
Kevin Lee, Zhengkun Ye and Angeliki Koutsoukou-Argyraki

We formalize the proofs of Cauchy's and Legendre's Polygonal Number Theorems
given in Melvyn B. Nathanson's book "Additive Number Theory: The Classical Bases".

... (see the url below)

We also formalize the proof of Gauss's theorem which states that every
non-negative integer is the sum of three triangular numbers.

https://www.isa-afp.org/entries/Polygonal_Number_Theorem.html

Enjoy!

smime.p7s

Last updated: Apr 28 2024 at 20:16 UTC