Теренс Тао пересобрал свою игру по логике с помощью кодирующего агента
Lean Grimoire
В 2018 году Теренс Тао выпустил «QED» — интерактивный учебник по логике высказываний и логике первого порядка, оформленный как крафтинг-игра, где правила логики применяются для вывода заключения из гипотез. Теперь он пересобрал её с помощью кодирующего агента под рабочим названием «Lean Grimoire»: появилась опция показывать текущее состояние игры в виде незавершённого доказательства в Lean, а ради забавы добавлен «фэнтези-режим», где утверждения становятся «зельями», а выражения — «свитками». Автор ищет игроков для тестирования.
Ради забавы я также добавил опцию играть в «фэнтези-режиме», где различные элементы игры изображаются с помощью фэнтезийного флейвора (например, математические утверждения становятся «зельями», математические выражения — «свитками» и так далее).
- torben-friis
Ну и бардак в этой обучающей игре.
Простите за негатив, но это вступление в стиле LLM едва можно разобрать, а эти элементы управления выглядят как недоделанный личный документ в Obsidian.
Странно такое видеть от Тао — помню, его математические заметки были вполне доступными и хорошо написанными.