" Стартап Axiom создал ИИ AxiomProver, генерирующий формально верифицированные доказательства.
Ключевое отличие от других ИИ-систем - каждое решение - это не ответ, а полное формальное доказательство на языке Lean, которое можно машинно верифицировать. Lean не принимает неправильные доказательства.
Стартап выявил 3 категории задач и вот, что они показывают:
1. Простое для людей, мучительное для формализации - задачи на матанализ. Человек смотрит на график и видит ответ. А чтобы ИИ записать это в Lean нужны сотни строк кода.
2. Задачи, которые AxiomProver неожиданно решил - комбинаторика и геометрия - исторически слабые места ИИ-систем. Нерешённые задачи IMO 2024 и 2025 как раз из этих областей.
AxiomProver решил обе такие задачи на Putnam.
3. Люди и ИИ решили по-разному задачи, например,
в задаче A4 люди интуитивно тянулись к алгебре. ИИ подошел к решению геометрически.
Главный вопрос - что делает математическую задачу сложной для ИИ?
То, что сложно людям, и то, что сложно ИИ - разные вещи. У людей есть интуиция, а у ИИ
— пока темнота. Теория «машинной сложности» — что структурно делает задачи лёгкими или трудными для автоматических доказательств— это открытое исследовательское направление.
