stringtranslate.com

Asistente de pruebas

Una sesión de prueba interactiva en CoqIDE, que muestra el script de prueba a la izquierda y el estado de la prueba a la derecha

En informática y lógica matemática , un asistente de pruebas o demostrador interactivo de teoremas es una herramienta de software que ayuda a desarrollar pruebas formales mediante la colaboración entre humanos y máquinas. Esto implica algún tipo de editor de pruebas interactivo u otra interfaz con la que un humano puede guiar la búsqueda de pruebas, cuyos detalles se almacenan en una computadora y algunos pasos son proporcionados por ella .

Un esfuerzo reciente dentro de este campo es hacer que estas herramientas utilicen inteligencia artificial para automatizar la formalización de las matemáticas ordinarias. [1]

Comparación de sistemas

Interfaces de usuario

Una interfaz popular para los asistentes de prueba es Proof General, basado en Emacs , desarrollado en la Universidad de Edimburgo .

Coq incluye CoqIDE, que se basa en OCaml/ Gtk . Isabelle incluye Isabelle/jEdit, que se basa en jEdit y la infraestructura Isabelle/ Scala para el procesamiento de pruebas orientado a documentos. Más recientemente, se han desarrollado extensiones de Visual Studio Code para Coq, [9] Isabelle por Makarius Wenzel, [10] y para Lean 4 por los desarrolladores de leanprover. [11]

Alcance de la formalización

Freek Wiedijk ha estado llevando un ranking de asistentes de demostración según la cantidad de teoremas formalizados de una lista de 100 teoremas conocidos. A septiembre de 2023, solo cinco sistemas han formalizado demostraciones de más del 70% de los teoremas, a saber, Isabelle, HOL Light, Coq, Lean y Metamath. [12] [13]

Pruebas formalizadas notables

La siguiente es una lista de pruebas notables que se han formalizado dentro de los asistentes de prueba.

Véase también

Notas

  1. ^ Ornes, Stephen (27 de agosto de 2020). "Quanta Magazine – ¿Qué tan cerca están las computadoras de automatizar el razonamiento matemático?".
  2. ^ Hunt, Warren; Matt Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith (2005). "Meta Reasoning in ACL2" (PDF) . Demostración de teoremas en lógica de orden superior . Apuntes de clase en informática. Vol. 3603. págs. 163–178. doi :10.1007/11541868_11. ISBN 978-3-540-28372-0.
  3. ^ abc "agda/agda: Agda es un lenguaje de programación de tipado dependiente / demostrador interactivo de teoremas". GitHub . Consultado el 31 de julio de 2024 .
  4. ^ "La Wiki de Agda" . Consultado el 31 de julio de 2024 .
  5. ^ Buscar "pruebas por reflexión": arXiv :1803.06547
  6. ^ "Página de lanzamientos de Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
  7. ^ "Versión v0.198 · ​​metamath/Metamath-exe". GitHub .
  8. ^ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier (1993). "IMPS: Un sistema interactivo de prueba matemática". Journal of Automated Reasoning . 11 (2): 213–248. doi :10.1007/BF00881906. S2CID  3084322 . Consultado el 22 de enero de 2020 .
  9. ^ "coq-community/vscoq". 29 de julio de 2024 – vía GitHub.
  10. ^ Wenzel, Makarius. "Isabelle" . Consultado el 2 de noviembre de 2019 .
  11. ^ "VS Code Lean 4". GitHub . Consultado el 15 de octubre de 2023 .
  12. ^ Wiedijk, Freek (15 de septiembre de 2023). "Formalizando 100 teoremas".
  13. ^ Geuvers, Herman (febrero de 2009). "Asistentes de prueba: Historia, ideas y futuro". Sādhanā . 34 (1): 3–25. doi : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 . S2CID  14827467.
  14. ^ Gonthier, Georges (2008), "Demostración formal: el teorema de los cuatro colores" (PDF) , Notices of the American Mathematical Society , 55 (11): 1382–1393, MR  2463991, archivado (PDF) desde el original el 2011-08-05
  15. ^ "Feit Thomson demostró en Coq - Microsoft Research Inria Joint Centre". 19 de noviembre de 2016. Archivado desde el original el 19 de noviembre de 2016. Consultado el 7 de diciembre de 2023 .
  16. ^ Licata, Daniel R.; Shulman, Michael (2013). "Cálculo del grupo fundamental del círculo en la teoría de tipos de homotopía". 28.° Simposio anual ACM/IEEE sobre lógica en informática de 2013. págs. 223–232. arXiv : 1301.3443 . doi :10.1109/lics.2013.28. ISBN 978-1-4799-0413-6. S2CID  5661377 . Consultado el 7 de diciembre de 2023 .
  17. ^ "Un problema matemático que se ha estado gestando durante 3500 años finalmente obtiene una solución". IFLScience . 2022-03-11 . Consultado el 2024-02-09 .
  18. ^ Avigad, Jeremy (2023). "Matemáticas y el giro formal". arXiv : 2311.00007 [math.HO].
  19. ^ Sloman, Leila (6 de diciembre de 2023). "El 'Equipo A' de matemáticas demuestra un vínculo crítico entre la suma y los conjuntos". Revista Quanta . Consultado el 7 de diciembre de 2023 .
  20. ^ "Hemos demostrado que "BB(5) = 47.176.870"". El desafío del castor atareado . 2024-07-02 . Consultado el 2024-07-09 .

Referencias

Enlaces externos

Catálogos