La automatización de pruebas con LLMs hace que Lean sea práctico

We have proof automation now

Adam Langley construyó un descompresor de Zstandard en Lean para explorar cómo los LLMs pueden automatizar la demostración de teoremas. Explica cómo la irrelevancia de la prueba, combinada con la capacidad de los LLMs para generar pruebas, reduce drásticamente el esfuerzo de probar invariantes en lenguajes con tipos dependientes. También ofrece una explicación clara del codificador de entropía FSE de Zstandard, destacando su diseño basado en estados que permite bits fraccionarios.