LATIDIA · Investigación

Formalizar problemas inversos en la era de la IA: posibilidades, trampas y una invitación

arXiv:2611.06962v1 Tipo de anuncio: nuevo Resumen: los asistentes de pruebas como Lean comprueban las pruebas matemáticas hasta los axiomas, y los agentes de IA han hecho recientemente que escribir tales pruebas sea barato. Describimos AutoIP, una biblioteca Lean i

La noticia

arXiv:2611.06962v1 Announce Type: new Abstract: Proof assistants such as Lean check mathematical proofs down to the axioms, and AI agents have recently made writing such proofs cheap. We describe AutoIP, a Lean library in which classical linear regularization theory, together with the functional analysis it rests on, has been autoformalized by AI agents. A machine-checked proof certifies only the formal statement it proves, so the remaining human task is to confirm that each formal statement says what was intended. We organize the library around this task: a reviewer compares the formal statements with their natural-language counterparts and never needs to read a proof. Our experience is that the risks lie