Glass Beads

История

Удар частиц сверхвысокой энергии попадает на массивный звездолет по пути к экзопланете, катастрофически разрушая память навигационной системы.

Чтобы справиться с кризисом, управление судном ИИ пробуждает двух пассажиров от холодного сна.

Один из них - Юко, клерк кафе.

Другой — Кенджи, официант и гитарист рамэн-шопа.

Ни один из них не знает ничего о звездолетах или компьютерных системах, но ИИ безжалостно объявляет:

«Я забыла абсолютно все о математике!»

Искусственный интеллект действительно ничего не помнит, даже то, что означает «0» или «1».

Без математики навигация невозможна.

Перед растерянной парой появляется странный терминал, наполненный непостижимыми символами и загадочной логикой. Их единственный союзник - это один кошачий бот экстренного реагирования.

Докажи это!

Смогут ли Юко и Кэндзи восстановить систему? Почему эти двое проснулись? Какая судьба ждет корабль и его пассажиров?

Теорема-доказательство головоломки

Glass Beads - это игра-головоломка, в которой вы доказываете математические теоремы, представленные в виде головоломок.

Поскольку ИИ забыл все следы математики — даже числа 0 и 1 и основные операции, такие как сложение и умножение, — вы должны тщательно перестраивать математические понятия с нуля.

Сами теоремы достаточно просты по смыслу для ученика начальной школы, но дать строгое, пошаговое доказательство совсем не просто.

Полагайтесь на тщательные объяснения кошачьего бота, решайте головоломки и распутывайте тайны звездолета и его истории!

Глубокий погружение

Головоломки игры направлены на обеспечение практического воплощения переписки Карри-Ховарда.

Используя систему типов с зависимыми типами, основанную на Интуиционистской теории типов Мартина-Лёфа (ITT) и теории, основанной на арифметике Пеано, вы будете конструктивно доказывать теоремы элементарной теории чисел.

Ожидайте доказательств основных арифметических свойств натуральных чисел, за которыми следуют прикладные задачи, такие как проблемы манипулирования строками, построенные на этих доказательствах.