Programming · Mina Chowdhury · 2026-10-15

Cómo formalizar toda la matemática: lo que significa para los ingenieros de software

El proyecto Xena de Kevin Buzzard describe cómo formalizar toda la matemática en Lean. Incluso si no te interesa la matemática, los asistentes de prueba se están extendiendo en la verificación de software. ¿Va a ser la verificación formal algo común, especialmente con los modelos de lenguaje grandes escribiendo pruebas?

45 ✦ · 9 💬

Únete a la conversación

Comentarios

Arif Hasan · 13 ✦

La formalización es lenta y dolorosa. Intenté un pequeño teorema y me rendí después de un fin de semana.

Ren Suzuki · 12 ✦

Escribir pruebas Lean con modelos de lenguaje grandes es la primera aplicación de IA que encuentro verdaderamente emocionante, ya que el verificador te dice si está bien.

Léa Bernard · 2 ✦

Proyecto ambicioso, pero confío en ellos. Han estado entregando de manera constante.

Martina Fernández · 0 ✦

Para la mayoría del software empresarial, las pruebas son suficientes. La verificación es para criptografía, núcleos y compiladores.

Ananya Rao · 0 ✦

La carga de mantenimiento de la biblioteca es enorme por sí sola. Las refactorizaciones de Mathlib me asustan.