🔧 MathCode — ШІ-асистент для формальних математичних доведень

Більшість ШІ-інструментів не підтримують формальну верифікацію теорем, а побудова власного пайплайну потребує значних витрат часу.

Ключові можливості:
• Конвертація математичних задач з природної мови у теореми Lean 4 з автоматичним доведенням
• Інтеграція з Lean LSP та бібліотекою Mathlib, автоматичне виправлення помилок компіляції (до 10 ітерацій)
• Паралельний запуск стратегій доведення та генерація графів залежностей для Obsidian

⚡️ Мова: Python 52.7%
🛠 Платформа: термінал, Lean 4

Переглянути репозиторій


Підписатися • GitHub 🇺🇦

#python #ai #ml #tools #linux