Talève
Talève is a formal model of stacker games in Lean.
Background
The modern stacker community has published many materials on setups and theory. However, this research is fragmented across various chat threads, wiki pages, and spreadsheets.
Talève aims to help by providing a standard method for researchers to formalize and publish their work.
Name
"Talève" is the French word for swamphen. Two species of the bird, pūkeko and takahē, are common in Aotearoa New Zealand. The name honors the author's birthplace, and follows the French tradition of naming software after animals.
The other word starting with "T"
The name of the first stacker game is trademarked, and the company that owns it is quite eager to shut down projects that mention it. So, to protect this project, I ask that we do not mention that name here.