MathCode — работа с кодом и доказательствами Lean 4
MathCode — помощник для написания кода в терминале и браузере, со встроенной поддержкой Lean 4. Он может проверять цели доказательств, искать объявления, проверять кандидатов и верифицировать завершённые доказательства.
Инструмент позволяет работать с кодом и доказательствами Lean в собственном рабочем пространстве. Он предлагает использование терминала или локального веб-интерфейса с рендерингом математических выражений и диаграмм. MathCode может хранить проверенные теоремы и явные предположения, а также исследовать зависимости в Obsidian. Проект позволяет добавлять навыки, инструменты анализа Python и плагины MCP.
Проект поддерживает macOS Apple Silicon (arm64) и Linux x86_64 с glibc и AVX2. Для работы требуется CLI codex и вход в систему Codex. Полная установка с поддержкой Lean требует около 10 ГБ дополнительного дискового пространства.
https://github.com/math-ai-org/mathcode | 745 звёзд
#сервисы
