Axiom Math formalizó el Stacks Project para demostrar que el vibe coding a gran escala puede ser riguroso

Axiom Math ha formalizado el Stacks Project, una referencia central de la geometría algebraica moderna, en código Lean, de modo que un ordenador puede verificar sus demostraciones línea por línea. Su enjambre de agentes trabajó como una organización de ingeniería, con humanos asignando equipos a la arquitectura, las definiciones centrales y las demostraciones individuales, y nada entró en la biblioteca sin que la lógica se sostuviera. El resultado es una biblioteca gratuita y de código abierto que cubre gran parte del campo, y un contraejemplo a la idea de que el vibe coding a gran escala solo produce chapuzas.

• Rohan Paul2026-11-04 17:53