Представлен проект MathCode — это терминальный помощник по программированию с ИИ со встроенным механизмом формализации математических формул. «Дайте ему математическую задачу на простом языке, и он автоматически преобразует её в теорему Lean 4 и попытается дать формальное доказательство — с помощью постоянно доступной интерактивной среды Lean REPL, многократно используемых библиотек теорем и аксиом, агентного доказательства и графа знаний Obsidian», — пояснили в команде проекта.