Glass Beads

Story An ultra‑high‑energy particle strike hits a massive starship en route to an exoplanet, catastrophically corrupting the navigation system’s memory. To handle the crisis, the ship’s management AI awakens two passengers from cold sleep. One is Yuko, a café clerk. The other is Kenji, a ramen‑shop waiter and guitarist. Neither knows the first thing about starships or computer systems, yet the AI pitilessly announces: “I’ve forgotten absolutely everything about mathematics!” The AI truly remembers nothing—not even what “0” or “1” mean. Without mathematics, navigation is impossible. A strange terminal appears before the bewildered pair, filled with inscrutable symbols and puzzling logic. Their only ally is a single cat‑shaped emergency‑response bot. “Prove it!” Can Yuko and Kenji restore the system? Why were these two awakened? What fate awaits the ship and its passengers? Theorem‑Proving Puzzle Glass Beads is a puzzle‑novel game in which you prove mathematical theorems presented as puzzles. Because the AI has forgotten every trace of mathematics—even the numbers 0 and 1 and basic operations like addition and multiplication—you must painstakingly rebuild mathematical concepts from scratch. The theorems themselves are simple enough in meaning for an elementary‑school student to grasp, yet giving a rigorous, step‑by‑step proof is anything but easy. Rely on the cat‑bot’s careful explanations, solve the puzzles, and unravel the mysteries of the starship and its story! A Deeper Dive The game’s puzzles aim to provide a hands‑on embodiment of the Curry–Howard correspondence. Using a type system with dependent types based on Martin‑Löf’s Intuitionistic Type Theory (ITT) and a theory grounded in Peano arithmetic, you will constructively prove theorems of elementary number theory. Expect proofs of basic arithmetic properties of natural numbers, followed by applied challenges such as string‑manipulation problems built upon those proofs.