Post #601

4-месячный стартап Axiom сообщил, что их ИИ AxiomProver решил 9 из 12 задач в языке Lean Axiom строит Ml-математика, способного на рассуждения, генерацию доказательств, проверку своей работы. Коммерческие последствия огромны - верификация, логистика, трейдинг, научные исследования и любые домены, где важны корректность и оптимизация Что именно сделал их Ml: - Задачи формализовали люди (это был внутренний «Prove-a-ton» — хакатон по переводу задач в Lean) - Дальше AxiomProver работал полностью автономно - 8 задач решены за первые 58 минут после экзамена, 9-я — к полудню следующего дня - Всё в Lean 4 + Mathlib, каждое доказательство проверено компилятором на 100 % Что говорят сами математики: 1. Это первый случай, когда Ml даёт полностью верифицируемые доказательства на уровне топ-5 мира 2. Формальные доказательства пока дорогие, но цена одного пруфа может превышать зарплату аспиранта 3. Через 5–10 лет такие системы будут обычным инструментом, как сейчас Wolfram Alpha, только для доказательств Основателем стартапа является 24-летняя Карина Хонг,окончившая MIT и получившая 2 диплома математика и физика за 3 года, также она лауреат Morgan Prize, Rhodes Scholar, бросила PhD/JD в Стэнфорде Недавно к ней присоединился Кен Оно — один из самых влиятельных ныне живущих специалистов по теории чисел и эллиптическим кривым (бывший вице-президент AMS, ментор десятков Putnam Fellows) Команда — 17 человек, среди них аспиранты и постдоки из MIT, Cambridge, Imperial, Humboldt Стартап привлек уже $64.000.000 от Menlo Ventures У кейс интересен тем, что уровень сложности экзаменов выше, чем IMO, которым хвастались Google, OpenAI, Harmonic Ml AxiomProver решил 12 из 12 задач самой сложной студенческой математической олимпиады в мире Putnam Стартап Axiom создал ИИ AxiomProver, генерирующий формально верифицированные доказательства Ключевое отличие от других Ml-систем - каждое решение - это не ответ, а полное формальное доказательство на языке Lean, которое можно машинно верифицировать Lean не принимает неправильные доказательства Стартап выявил 3 категории задач и вот, что они показывают: 1. Простое для людей, мучительное для формализации - задачи на матанализ Человек смотрит на график и видит ответ А чтобы Ml записать это в Lean нужны сотни строк кода 2. Задачи, которые AxiomProver неожиданно решил - комбинаторика и геометрия - исторически слабые места Ml-систем Нерешённые задачи IMO 2024 и 2025 как раз из этих областей AxiomProver решил обе такие задачи на Putnam 3. Люди и Ml решили по-разному задачи, например, в задаче A4 люди интуитивно тянулись к алгебре Ml подошел к решению геометрически Главный вопрос - что делает математическую задачу сложной для Ml? То, что сложно людям, и то, что сложно Ml - разные вещи У людей есть интуиция Теория «машинной сложности» — что структурно делает задачи лёгкими или трудными для автоматических доказательств— это открытое исследовательское направление