Post #843

На переднем крае математики сейчас происходят сразу несколько сдвигов, и все они так или иначе связаны с искусственным интеллектом Один из самых интересных — переход от неформальной «бумажной» математики к формальной, в которой каждое утверждение и каждое доказательство представлены в виде точного кода, который проверяет компьютер Интерактивные системы доказательства теорем вроде Lean и Coq стали не просто экзотикой, а рабочими инструментами, позволяющими записывать сложные теории в виде формальных систем и получать гарантию, что в цепочке рассуждений нет ни одной пропущенной детали На этом фоне появилась новая практическая область — то, что я бы назвал «математикой с поддержкой AML» Это когда большая языковая модель не придумывает теоремы из воздуха, а помогает математику и инженеру проходить самые рутинные, трудоёмкие части работы: подбирать тактики, искать подходящие леммы в огромной библиотеке, заполнять фрагменты доказательств Мои собственные эксперименты показывают, что в связке «человек + модель» можно автоматически закрывать значительную часть шагов в доказательстве, сокращая руками вводимые тактики в Lean в разы по сравнению с классическими средствами автоматизации Это уже не теория, а рабочие прототипы, которые используются в реальных проектах Параллельно растёт направление полностью автоматического доказательства: системы вроде AlphaProof и других нейросетевых связок учатся по библиотекам формальных доказательств, генерируют собственные доказательства и находят ошибки в существующих формулировках Они особенно сильны там, где структура теоремы и используемых понятий уже хорошо отражена в формальной библиотеке, и пока заметно слабее на действительно новых концепциях, но в связке с человеком дают эффект, которого у классических автоматических систем просто не было Это меняет не только темп работы, но и саму практику: становится возможным проверять и дорабатывать формулировки, с которыми математики жили десятилетиями Для инженера по искусственному интеллекту всё это не «чужая наука», а ближайшее будущее профессии От формальной верификации критичных систем до проверки корректности протоколов и сложных алгоритмов — везде, где цена ошибки велика, математические доказательства становятся частью инженерного процесса, а инструменты с AML-поддержкой снимают барьер входа в формальную математику Понимать, что именно делает такая система, где границы её возможностей, чем отличается формальное доказательство от красивого, но нестрогого эскиза — всё это требует дискретного и логического фундамента Если коротко: математика перестаёт быть исключительно «бумажной наукой» и всё больше становится совместной работой человека и машины — с формальными языками, проверяемыми доказательствами и AML-помощниками И специалист, который в этом не разбирается, через несколько лет будет таким же анахронизмом, как программист, не умеющий пользоваться системой контроля версий