Relación entre el número e y los números primos en Maxima

PorJosé A. Alonso

En el artículo anterior comenté la relación entre los números primos y el número e expresada mediante la fórmula


e = \displaystyle\lim_{n \to{+}\infty}\displaystyle\sqrt[p_n]{\displaystyle\prod_{i=1}^n p_i}

donde p_i es el i-ésimo número primo. Así mismo mostré un ejercicio en Haskell para comprobarla.

En el artículo de hoy presento un ejercicio para comprobar la fórmula anterior en Maxima, pensado para el curso de Informática (del Grado de Matemáticas) y el libro Introducción al cálculo simbólico con Maxima.

El ejercicio es el siguiente

Read More “Relación entre el número e y los números primos en Maxima”

Relación entre el número e y los números primos en Haskell

PorJosé A. Alonso

En el artículo ¿Qué tiene que ver el número e con los números primos? de Gaussianos se comenta una curiosa relación entre los números primos y el número e. Dicha relación se expresa mediante la fórmula


e = \displaystyle\lim_{n \to{+}\infty}\displaystyle\sqrt[p_n]{\displaystyle\prod_{i=1}^n p_i}

donde p_i es el i-ésimo número primo.

A partir del artículo, he diseñado este ejercicio de Haskell para Informática (del Grado de Matemáticas).

El objetivo del ejercicio es la comprobación de la fórmula anterior.
Read More “Relación entre el número e y los números primos en Haskell”

Ventajas de la pereza en el problema de los k menores elementos

PorJosé A. Alonso

Una característica singular de Haskell es su carácter perezoso, frente al impaciente de la mayoría de los restantes lenguajes.

Los lenguajes perezosos usan evaluación perezosa; es decir, al evaluar una expresión evalúan sus argumentos sólo cuando los necesita. De manera opuesta, en la evaluación impaciente los argumentos de las expresiones se evalúan antes que las expresiones.

En esta entrada presento un ejercicio para Informática (del Grado de Matemáticas) con objeto de resaltar la ventaja de la evaluación perezosa de Haskell frente a la evaluación impaciente de Maxima. Para ello compararé sus rendimientos al calcular los k primeros elementos de una lista con definiciones semejantes en Haskell y Maxima.
Read More “Ventajas de la pereza en el problema de los k menores elementos”

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”

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

PorJosé A. Alonso

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”