¿Hay una base de datos canónica de teoremas?

Question

¿Existe una base de datos (pública) de teoremas, ya que las secuencias enteras están catalogadas en la Enciclopedia en línea de las secuencias de enteros (OEIS)?

Answer 1

El Metamath Prueba Explorer "... tiene más de 12,000 totalmente trabajado a cabo pruebas ..." [1] accesible a través de un índice, el teorema de la lista. [2] Cada teorema tiene su correspondiente etiqueta única.

El principal Metamath página se describe el proyecto, el Metamath idioma, y los programas y bases de datos disponibles para su uso. [3] El Metamath pruebas mecánicas, y puede o no ser útil a causa de su tedio y falta de perspectiva.

Una alternativa a Metamath es Ghilbert [4], que se ve mucho más bonito. Por ejemplo, el contraste de la Ghilbert la prueba del Teorema de Euclides [5] con el Metamath prueba de una infinidad de números primos. [6] por Desgracia, Ghilbert no parece tener un índice de la base de datos de teoremas como Metamath.

Algunas ad hoc listas de teoremas que no incluyen canónica identificadores son:

• https://en.wikipedia.org/wiki/List_of_theorems
• https://en.wikipedia.org/wiki/List_of_mathematical_proofs
• http://www.regentsprep.org/Regents/math/geometry/GPB/theorems.htm

El Cortar el Nudo y Wolfram Mathworld sitios web, vale la pena mencionar, aunque sólo sea porque tiene una extensa colección de recursos matemáticos, muchos de los teoremas incluido.

La siguiente es una lista de algunas de las respuestas correspondientes en las matemáticas.SE. Sin embargo, estas respuestas no dirección canónica de la indexación de los teoremas.

• El más común de los teoremas enseñado en Álgebra Abstracta
• ¿Alguien sabe de un sitio que tiene un conjunto de todos los teoremas?

Referencias:

• [1] http://us.metamath.org/mpegif/mmset.html#overview
• [2] http://us.metamath.org/mpegif/mmtheorems.html (en línea imágenes GIF) y http://us.metamath.org/mpeuni/mmtheorems.html (unicode)
• [3] http://us.metamath.org/
• [4] http://ghilbert-app.appspot.com/
• [5] http://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/euclidthm
• [6] http://us.metamath.org/mpegif/mmtheorems99.html#mm9884s

Answer 2

También podría agregar que ProofWiki es un proyecto comunitario para hacer eso, completo con pruebas.