Axiom Math formalizou o Stacks Project para mostrar que o vibe coding em larga escala pode ser rigoroso

A Axiom Math formalizou o Stacks Project, uma referência central da geometria algébrica moderna, em código Lean, de modo que um computador agora pode verificar suas demonstrações linha por linha. Seu enxame de agentes trabalhou como uma organização de engenharia, com humanos designando equipes para arquitetura, definições centrais e demonstrações individuais, e nada entrou na biblioteca sem que a lógica se sustentasse. O resultado é uma biblioteca gratuita e de código aberto que cobre grande parte do campo, e um contraexemplo à ideia de que o vibe coding em larga escala só produz trabalho descuidado.

• Rohan Paul2026-11-04 17:53