Email Gateway (Aug 22 2022 at 18:30): Email Gateway (Aug 22 2022 at 18:30):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Andrei wrote:
I formalized the classical nontrivial result that harmonic numbers are not integers, except for 1 (I think that this is new in Isabelle). Also, some theorems about Pythagorean triangles and perfect powers. Feel free to take a look if some of these theorems are interesting for the list (the statements of the theorems are at the begging of the thy file) https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory
Kind Regards,
Jose M.
Last updated: Apr 18 2024 at 01:05 UTC