Axiom Math формализовала проект Stacks, показав, что вайб-кодинг в масштабе может быть строгим

Axiom Math формализовала проект Stacks — ключевой справочник современной алгебраической геометрии — в код Lean, так что компьютер теперь может проверять его доказательства строка за строкой. Рой её агентов работал как инженерная организация: люди распределяли команды по архитектуре, основным определениям и отдельным доказательствам, и в библиотеку попадало только то, чья логика выдерживала проверку. Результат — бесплатная библиотека с открытым исходным кодом, охватывающая большую часть области, и опровержение идеи, что вайб-кодинг в масштабе даёт лишь небрежный код.

• Rohan Paul2026-11-04 17:53