🚀 В недавнем посте я рассказывал о прототипе инструмента для автоматической проверки математических оценок. С тех пор он претерпел две крупные доработки:
1. Сначала превратился в базовый proof assistant с поддержкой пропозициональной логики.
2. Затем стал гибким ассистентом, вдохновлённым Lean, с интеграцией символьной алгебры через Python-библиотеку Sympy 🧮. Это стало возможным благодаря фидбеку сообщества!
Теперь это стабильная платформа, которую можно расширять: добавлять тактики, типы данных и леммы для решения широкого круга задач.
Как это работает?
Инструмент работает в интерактивном режиме Python (напоминает текстовые квесты для старшего поколения 🎮). Пример сессии:
“`python
>>> from main import *
>>> p = linarith_exercise()
Задача: доказать x < 7z + 2 при условиях x < 2y и y < 3z + 1
>>> p.use(Linarith(verbose=True)) # Решаем линейной арифметикой с детализацией
“`
Результат: автоматическое доказательство через суммирование неравенств ✅.
Сложные случаи
Для задач с ветвлением (например, доказательство (x + y > -3) & (x + y < 3)) инструмент строит древовидную структуру доказательства:
“`python
p.use(SplitHyp(“h1”)) # Разбиваем гипотезы
p.use(SplitGoal()) # Делим цель на подзадачи
p.use(Linarith()) # Решаем каждую часть
“`
Итог: псевдо-Lean код доказательства 🌳.
Асимптотики и вызовы
С помощью Sympy реализована работа с порядками величин (Θ-нотация). Например:
“`python
p.use(LogLinarith(verbose=True)) # Логарифмическая линейная арифметика
“`
Но есть нюансы: текущая версия плохо обрабатывает выражения с `Max` (например, `Max(Θ(1), Θ(N))`). Для таких случаев требуется ручное применение тактик — это в планах доработки 🔧.
Будущее проекта
В разработке:
- Тактики для норм функциональных пространств (неравенства Гёльдера, Соболева) 📐
- Расширение типов данных и лемм в Sympy
- Приветствуются идеи и вклад сообщества: новые задачи, тактики, исправления! 💡
👉 Итог: Инструмент уже мощный, но потенциал роста огромен. Попробуйте [здесь](ссылка) и предлагайте улучшения!