Axiom Math: формальным доказательствам нужно больше, чем корректность

Axiom Math рассматривает формализованную математику, создаваемую ИИ, на трёх уровнях: корректность, качество кода на Lean и математический вкус. Доказательство может быть формально корректным, но при этом считаться слабым из-за небрежной структуры или реализации.

В формализации результата о разрывах, выполненной Polymath AB, Axiom делала акцент на повторно используемом коде Lean и качестве, которое позволит другим сообществам развивать эту работу. Компания также считает, что человеческое суждение по-прежнему важно для определения того, какие теоремы имеют значение и могут найти полезные применения в реальном мире.