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.
Los teoremas del punto fijo de Cartan formalizados son los siguientes:
- (Primer teorema de Cartan) Sea
un dominio acotado,
una función holomórfica y
. Si
y el diferencial
de
en
es la función identidad, entonces
- (Segundo teorema de Cartan) Sea
cony
un automorfismo holomórfico de
tal que
. Entonces,
.
- (Aplicación del segundo teorema de Cardan) El grupo de todos los automorfismos holomórficos de la bola abierta unidad de
Como sistema para la formalización han elegido HOL Light ya que cuenta con muchas teorías formalizadas para análisis complejo.
Las teorías desarrolladas en Hol Light son:
- Library/iter.ml para propiedades de la iteración de aplicaciones de una función;
- Multivariate/canal.ml para los resultados sobre la analiticidad en el entorno de un punto;
- Multivariate/cauchy.ml para las demostraciones del primer y segundo teorema de Cardan;
- Examples/moebius.ml para las funciones de Möbius y la clasificación de los automorfismos del disco unidad.
En A Formalization of Cartan’s theorem in HOL se encuentran todas las teorías juntas y un esquema de la demostración.
Entre las dificultades que comentan loa autores en la realizaión de la formalización destacan los siguientes:
- La dificultad de comenzar a usar el sistema de razonamiento y de buscar los lemas adecuados para la demostración. La existencia de gran cantidad de conocimiento formalizado es una facilidad pero su reutilización es difícil, aunque la dificultad se ve aliviada con la ayuda del buscador de lemas que posee HOL Light.
- El estilo de demostración ha sido procedural en lugar de declarativo (como Mizar, Isar o C-zar) lo que dificulta la lectura de las pruebas por parte de las personas. Esta dificultad es especialmente notable en los casos de demostración de resultados matemáticos donde la prueba es tan interesante como el resultado que se demuestra.
La formalización es compacta (con un factor de Bruijn de 3.5) y muesta la viabilidad de aplicar el razonamiento formalizado a teoremas importantes del análisis complejo. y puede continuarse formalizando otros rsultados del análisis complejo.
Finalmente, me parece una idea interesante la formalización de resultados matemáticos importantes y relativamente recientes (por ejemplo, los demostrados en el siglo XX). Comenzaré su elaboración en la siguiente entrada.