¿Cómo organiza el asistente de pruebas los conocimientos?

Question

Estoy leyendo un artículo

Ittay Weiss, El Manifiesto QED después de dos décadas - Versión 2.0 , Journal of Software, 11 no. 8 (2016) pp. 803-815, doi: 10.17706/jsw.11.8.803-815

El documento dice

Objetivo 7: Organización del conocimiento. El volumen de conocimientos matemáticos es asombroso. No sólo la totalidad de las matemáticas está más allá del alcance del dominio de una sola persona, sino que lo mismo puede decirse de cada una de las principales áreas de las matemáticas (por ejemplo, topología, álgebra, análisis, lógica, etc.). Además, cada año se acumula una cantidad abrumadora de nuevas matemáticas. Tanto para los usuarios de las matemáticas como para los matemáticos novatos y expertos, navegar por el océano de resultados se está convirtiendo en una habilidad que parece requerir capacidades sobrehumanas. Tanto QED 1.0 como QED 2.0 pretenden ofrecer herramientas inestimables para este fin. El sistema dispondrá de herramientas para navegar, buscar y comparar resultados. Analizando las interdependencias en la codificación de varios resultados, el sistema podrá localizar automáticamente resultados similares sospechosos de estar relacionados (o quizás duplicados), identificando así áreas de las matemáticas que están más relacionadas de lo que parece.

Creo que organizar el conocimiento es realmente importante para la demostración interactiva de teoremas (ITP). Especialmente, quiero averiguar el estado de la comparación, el análisis de las matemáticas representadas por ITP. Pero no puedo encontrar ningún proyecto o trabajo sobre la comparación y el análisis de las matemáticas representadas por ITP. ¿Podría recomendarme algunos trabajos o proyectos relacionados con la comparación y el análisis de las matemáticas mediante ITP?

Answer 1

La organización de las matemáticas en forma computarizada es un tema algo distinto de la demostración automatizada y asistida de teoremas. He aquí algunas indicaciones que le permitirán empezar:

• MathWebSearch Un motor de búsqueda de fórmulas matemáticas basado en el contenido
• OpenMath Normas para representar la semántica de los objetos matemáticos y comunicarlos entre sistemas de software
• El sistema lingüístico de MMT para la representación del conocimiento matemático

Un tema típico en la organización del conocimiento matemático es cómo representar el conocimiento matemático de una manera independiente de la plataforma, agnóstica con respecto a los fundamentos matemáticos (o al menos traducible entre fundamentos), y fácilmente buscable. Nada de esto es fácil de resolver. Se podría pensar, por ejemplo, que todos podríamos ponernos de acuerdo en algunos para representar fórmulas, pero ese no es el caso. ¿Debemos utilizar la lógica de primer orden, la lógica de orden superior o la teoría de tipos? ¿Qué operaciones de metanivel en las teorías formales debemos admitir? ¿Quién gobierna las convenciones de denominación de los lemas, teoremas y definiciones? Y hay metateoremas que demuestran que averiguar si dos teoremas "afirman lo mismo" es un problema computacional muy difícil, incluso para fragmentos de lógica muy simples.

Personalmente, creo que estos esfuerzos son inmensamente importantes, pero también que no debemos esperar que den lugar a una gran unificación del conocimiento matemático. La visión aceptada de los fundamentos matemáticos es que, seguramente, toda la matemática puede unificarse como un todo coherente en un único sistema. Sin embargo, si se mete a un grupo de expertos en fundamentos matemáticos en una habitación y se les encierra hasta que se pongan de acuerdo en uno en particular formalismo matemático que sirva para expresar toda la matemática, se morirán de sed antes de ponerse de acuerdo en algo. No creo que esto sea culpa de los lógicos o de la lógica. Tiene algo más profundo que ver con la forma en que los sistemas multiagentes (como a los informáticos les gusta llamar a las colecciones de entidades inteligentes) organizan el conocimiento.

Answer 2

Por supuesto, una parte difícil es saber si dos lemas de aspecto similar están realmente relacionados, y aún más si dos enunciados superficialmente muy diferentes pueden tener una prueba breve de su equivalencia. Este artículo de ITP (Interactive Theorem Proving) parece prometedor:

Demostración de teoremas asistida por el aprendizaje con millones de lemas

Cezary Kaliszyk y Josef Urban https://doi.org/10.1016/j.jsc.2014.09.032