Терренс Тао, один из крупнейших математиков современности и лауреат Филдсовской премии, в интервью каналу Math Inc рассказал о трансформации математики под влиянием ИИ и формальных систем доказательств. По его словам, сочетание языков вроде Lean с нейросетями меняет саму природу математической работы — от одинокого ремесла к коллективной разработке, похожей на создание программного обеспечения. Читать далее