Impossibility of the Dissection of a Cube (Q7361730)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Cube_Dissection
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Impossibility of the Dissection of a Cube |
AFP entry Cube_Dissection |
Statements
22 November 2024
0 references
Thomas Holme Surlykke
0 references
Impossibility of the Dissection of a Cube (English)
0 references
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.
0 references
