Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Wieferich–Kempner Theorem ...

Email Gateway (Mar 08 2024 at 09:06):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I’m happy to announce a new AFP entry by Jamie Chen:

Wieferich–Kempner Theorem

This document presents a formalised proof of the Wieferich–Kempner Theorem,
stating that all nonnegative integers can be expressed as the sum of nine
nonnegative cubes. The source of the proof is the book "Additive Number Theory:
The Classical Bases" by Melvyn B. Nathanson.

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

Enjoy,
René

Last updated: Jun 20 2025 at 12:44 UTC