Email Gateway (Nov 25 2024 at 16:34): Email Gateway (Nov 25 2024 at 16:34):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce the contribution "Impossibility of the Dissection of a Cube", by Thomas Holme Surlykke. It’s on the famous list of 100 theorems, taking Isabelle to 91, well above HOL Light at 87.
This entry formalizes Littlewood's argument, demonstrating that a 3-dimensional cube cannot be dissected into a finite collection of smaller cubes, each of a different size. The formalization addresses theorem #82, "Dissection of Cubes (J.E. Littlewood's 'elegant' proof)" from Freek Wiedijk's "100 Mathematical Theorems" list, and is based upon a prior formalization in Lean.
https://www.isa-afp.org/entries/Cube_Dissection.html
Larry Paulson
Last updated: Feb 05 2025 at 16:23 UTC