Un reciente intento de refutar la conjetura de Collatz, cuya presunta refutación fue verificada en el asistente de pruebas Lean y contrastada con el comprobador independiente Nanoda, resultó ser erróneo: la demostración aprovechaba un fallo en el núcleo de Lean y Nanoda tampoco detectó el problema. El episodio ilustra una crítica de fondo al diseño de buena parte de los asistentes de pruebas contemporáneos: la acumulación de objetos de demostración como certificados verificables de forma independiente. En la práctica, no consta ningún caso en que un comprobador externo haya detectado un error de solidez que el núcleo del asistente hubiera dado por bueno; antes bien, estos certificados añaden una carga de memoria considerable sin protección real. El artículo contrasta dos filosofías de diseño. La primera, dominante en la actualidad, introduce en el núcleo numerosos elementos (tipos inductivos anidados en Lean, pattern matching con funciones recursivas en Rocq) por comodidad de implementación, a costa de aumentar la superficie de fallo. La segunda, heredera del trabajo de Russell y de la teoría de conjuntos y de tipos simples, construye por 'trabajo honesto' —a partir de axiomas mínimos— las definiciones inductivas, las funciones recursivas, el pattern matching y la recursión parcial, situándolas fuera del núcleo. Isabelle, HOL Light y HOL4 son ejemplos de esta segunda escuela: pocas reglas primitivas, gran expresividad derivada y, en consecuencia, menos bugs de solidez. La conclusión es que, si la prioridad es la solidez, los sistemas con núcleos minimalistas son la opción más segura.
Noticias agregadas con IA