Los principales teoremas del siglo XX y su formalización

PorJosé A. Alonso

Como comentaba en la entrada anterior, un gran reto para el razonamiento formalizado podría consistir en la formalización de los principales teoremas del siglo XX.

Este reto es análogo a Formalizing 100 Theorems que consiste en la formalización de los 100 principales teoremas de todos los tiempos.

El punto de partida ha de ser la determinación de cuáles son los principales teoremas del siglo XX y en qué punto se encuentra su formalización.

Algunos candidadatos de la lista de los principales teoremas del siglo XX son
Read More “Los principales teoremas del siglo XX y su formalización”

Reanudación

PorJosé A. Alonso

Después de 4 meses, reanudo la escritura en Vestigium. Como uno de sus objetivos era servir de diario de las publicaciones en mi sitio en la Red, voy a resumir las realizadas desde la anterior entrada en Vestigium.

He publicado una introducción al sistema de cálculo simbólico Maxima que he usado en las asignaturas de I1M (Informática de 1º de Matemáticas) como en la de SLEAM (Sofware libre para la enseñanza y aprendizaje de las Matemáticas). Los temas y ejercicios publicados son los siguientes:

las relaciones de ejercicios:

Además, en I1M (Informática de 1º de Matemáticas) he publicado dos nuevos temas sobre diseño de algoritmos con Haskell:

En la página de publicaciones he añadido las dos más recientes:

Finalmente, en la wiki del Grupo de Lógica Computacional he añadido las formalizaciones de teorías en PVS:

Razonamiento formalizado en análisis numérico

PorJosé A. Alonso

Hoy se ha publicado en arXiv el artículo Formal Proof of a Wave Equation Resolution Scheme: the Method Error escrito por Sylvie Boldo (INRIA Saclay – Ile de France, LRI), Francois Clement (INRIA Rocquencourt), Jean-Christophe Filliâtre (INRIA Saclay – Ile de France, LRI), Micaela Mayero (LIPN, INRIA Rhône-Alpes / LIP Laboratoire de l’Informatique du Parallélisme), Guillaume Melquiond (INRIA Saclay – Ile de France, LRI) y Pierre Weis (INRIA Rocquencourt).

En este trabajo se presenta una formalización en Coq de una parte del conocimiento matemático más usado en las ingeniería: las ecuaciones diferenciales. Curiosamente las ecuaciones diferenciales apenas se han tratado dentro del razonamiento formalizado.

Read More “Razonamiento formalizado en análisis numérico”

Advances and Perspectives in the Mechanization of Mathematics

PorJosé A. Alonso

Un indicador de la vitalidad de un área lo constituye los números especiales de revistas dedicadas al área.

La revista Mathematical Structures in Computer Science ha anunciado un número especial sobre Advances and Perspectives in the Mechanization of Mathematics.

En el anuncio se constata el éxito obtenido formalizando algunos teoremas matemáticos importantes tales como el teorema de los números primos, el teorema de los cuatro colores y el teorema de la curva de Jordan.

El número desea reflejar los avances recientes y las nuevas perspectivas dentro del campo de la formalización del conocimiento matemático, incluyendo descripciones de nuevas formalizaciones.

La fecha límite para el envío de artículos es el 28 de Junio de 2010.