Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in the AFP: Zeckendorf’s Theorem

view this post on Zulip Email Gateway (Jun 14 2023 at 11:05):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new contribution: a formalisation of Zeckendorf’s Theorem, by Christian Dalvit. The theorem states that every positive integer can be uniquely represented as a sum of one or more non-consecutive Fibonacci numbers. The proof formalises one given by Gerrit Lekkerkerker, who seems to have discovered this result first.

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

Larry Paulson

Last updated: Jan 04 2025 at 20:18 UTC