GPT-5.6-Sol-Ultra написала клон Minecraft на языке Lean

Питер Гостев показал: GPT-5.6-Sol-Ultra собрала клон Minecraft на Lean - языке для формальных доказательств, не для игр. По его словам, модель настолько сильна в математике, что вытянула нетипичную для языка задачу.

Почему это важно: Lean - это proof assistant, на нём пишут математические доказательства, а не игровую логику. Собрать на нём интерактивный клон Minecraft - редкий стресс-тест для рассуждений модели, а не для стандартной кодогенерации. Пример пока один, от одного человека, без кода и пруфов в твите.

Что дальше: Ждём публикацию репозитория или демо, чтобы проверить, что клон реально запускается и играбелен.