Reseña: A certified proof of the Cartan Fixed Point Theorems

Gianni Ciolli, Graziano Gentili y Marco Maggesi han publicado el artículo A Certified Proof of the Cartan Fixed Point Theorems en el Journal of Automated Reasoning. Una versión del artículo puede leerse aquí.

Los autores son profesores del Departamento de Matemáticas “Ulisses Dini” de la Universidad de Florencia. Los dos primeros son especialistas en geometría algebraica y análisis complejo y el tercero trabaja en razonamiento automático con Coq y HOL Light.

El objetivo del artículo es la aplicación del razonamiento formalizado a temas de investigación de la matemática contemporánea. Para ello han elegido como objetivo la formalización de los teoremas de Cartan del punto fijo, demostrados por Henri Cartan en 1930. Los teoremas elegidos son relativamente recientes y de gran importancia en el análisis complejos y campos relacionados.
Read More “Reseña: A certified proof of the Cartan Fixed Point Theorems”