Andrew Granville sabe que la inteligencia artificial cambiará profundamente las matemáticas. El lenguaje de programación Lean ya desempeña un papel en la demostración de la teoría. Es por eso que el teórico de números de la Universidad de Montreal ha comenzado a hablar con filósofos sobre la naturaleza de la prueba matemática y cómo la disciplina de las matemáticas podría evolucionar en la era de la IA.
#12:
#10 Puedo intentarlo yo? Desconozco tu punto de partida así que disculpa si te parece demasiado simplificado o demasiado impreciso (pero correcto en lo esencial). Imagina un cuerpo axiomático no trivial. Imagina esto simplemente como un conjunto de enunciados (axiomas) de los que puedes extraer conclusiones lógicas (si fuese trivial, no podrías). Es decir, crear nuevos enunciados a partir de los ya existentes.
Por ejemplo, empiezas con: "0 es un número natural", "todo número natural tiene un sucesor que también es un número natural"... y otros... Entonces, a partir de la afirmación de que existe un sucesor, por ejemplo, puedes "deducir" (y demostrar dentro del contexto que has establecido) que existe la suma, expresarlo formalmente, y seguir construyendo la aritmética, por ejemplo.
Lo que viene a decir esto es que no existe teoría alguna en la que no existan ciertos enunciados posibles que no se pueden demostrar de ningún modo a partir de los ya existentes. Siempre puedes buscar alguno que es indecidible. Esto quiere decir que las combinaciones de los enunciados que ya tienes no te permiten deducir si el nuevo es cierto o no.
La solución es añadir un nuevo axioma que decida ese caso que sea consistente con todos los demás (básicamente estás diciendo "este caso que no estaba resuelto es así por esta nueva información que no contradice nada de lo otro"), pero el resultado (consecuencia de los teoremas de incompletitud) será que, añadiendo un enunciado nuevo, estás engendrando aún más posibilidades de nuevos enunciados que son indemostrables a menos que añadas nuevos axiomas a su vez. Y, cuando añades nuevos enunciados, los nuevos enunciados indemostrables posibles crecen a un ritmo aún más rápido. De modo que, cualquier construcción de una teoría matemática autoconsistente que puedas llevar a cabo, estará siempre (y cada vez más) incompleta.
Pienso lo mismo. Para mí el problema llegará cuando la máquina escriba proposiciones que no podamos seguir, que podamos comprobar que son correctas pero, o bien no seamos capaces de seguir la secuencia deductiva que lleva a la máquina a hacer una afirmación, o no podamos seguir la demostración matemática (esto parece menos probable). Pero sobre todo cuando la máquina simplemente 'lo sepa' y no podamos saber por qué.
Pues que, al igual que los humanos, no pueden encontrar la prueba de todo enunciado matemático cierto porque es un problema no computable. Es más, hay enunciados matemáticos ciertos que ningún teorema puede demostrar: https://es.wikipedia.org/wiki/Teoremas_de_incompletitud_de_G%C3%B6del
#10 Puedo intentarlo yo? Desconozco tu punto de partida así que disculpa si te parece demasiado simplificado o demasiado impreciso (pero correcto en lo esencial). Imagina un cuerpo axiomático no trivial. Imagina esto simplemente como un conjunto de enunciados (axiomas) de los que puedes extraer conclusiones lógicas (si fuese trivial, no podrías). Es decir, crear nuevos enunciados a partir de los ya existentes.
Por ejemplo, empiezas con: "0 es un número natural", "todo número natural tiene un sucesor que también es un número natural"... y otros... Entonces, a partir de la afirmación de que existe un sucesor, por ejemplo, puedes "deducir" (y demostrar dentro del contexto que has establecido) que existe la suma, expresarlo formalmente, y seguir construyendo la aritmética, por ejemplo.
Lo que viene a decir esto es que no existe teoría alguna en la que no existan ciertos enunciados posibles que no se pueden demostrar de ningún modo a partir de los ya existentes. Siempre puedes buscar alguno que es indecidible. Esto quiere decir que las combinaciones de los enunciados que ya tienes no te permiten deducir si el nuevo es cierto o no.
La solución es añadir un nuevo axioma que decida ese caso que sea consistente con todos los demás (básicamente estás diciendo "este caso que no estaba resuelto es así por esta nueva información que no contradice nada de lo otro"), pero el resultado (consecuencia de los teoremas de incompletitud) será que, añadiendo un enunciado nuevo, estás engendrando aún más posibilidades de nuevos enunciados que son indemostrables a menos que añadas nuevos axiomas a su vez. Y, cuando añades nuevos enunciados, los nuevos enunciados indemostrables posibles crecen a un ritmo aún más rápido. De modo que, cualquier construcción de una teoría matemática autoconsistente que puedas llevar a cabo, estará siempre (y cada vez más) incompleta.
#23 Bueno, genera pruebas de forma automática a problemas que son descritos en ese lenguaje.
De hecho, basándose en la fuerza bruta, en la teoría, es muy fácil generar pruebas de forma automática si tratas un cuerpo axiomático como un lenguaje regular. Sólo tienes que generar todas las combinaciones posibles para ir generando todos los teoremas posibles junto con sus pruebas. Otra cuestión es que la mayor parte de los resultados sean inútiles, y nunca se acaban...
#1 Me temo que en 10 o 20 años cada vez menos matematicos van a ser capaces de refutar o validar las pruebas sin ayuda de otras computadoras.
Dicho esto, creo que la pareja humano-maquina sera como se innove por muchos años. Viene pasando en el ajedrez y ya hacen mas de 30 años que Deep Blue ganos sobre a los humanos
Pienso lo mismo. Para mí el problema llegará cuando la máquina escriba proposiciones que no podamos seguir, que podamos comprobar que son correctas pero, o bien no seamos capaces de seguir la secuencia deductiva que lleva a la máquina a hacer una afirmación, o no podamos seguir la demostración matemática (esto parece menos probable). Pero sobre todo cuando la máquina simplemente 'lo sepa' y no podamos saber por qué.
#2 al igual que en otras muchas materias, hace décadas que en física nadie es capaz de refutar nada sin un acelerador de partículas, por ejemplo ¿Porqué las matemáticas iban a ser diferentes?
#8 Porque la física es experimental al ser modelos que tratar de parametrizar la realidad. Las matemáticas no. La física teórica solo es teoría hasta que se refuta experimentalmente.
#20 En una determinada frecuencia, puedes empezar enviando secuencias de pulsos según los números primos: dos pulsos, tres pulsos, cinco pulsos... "pip-pip pip-pip-pip ..." Esto despertaría la curiosidad de cualquier observador.
A continuación (después de llegar a 1009 por ejemplo), explicas que vas a usar la numeración binaria: mandas un pulso seguido de 000001 pulsos (siendo 0 un lapso sin pulso que dure lo mismo que el pulso), mandas dos pulsos seguidos de 000010,... y así sucesivamente. La longitud de tus bytes (6 bits en este ejemplo) es arbitraria.
Lo siguiente es explicar los conceptos matemáticos y lógicos básicos. El primero es el operador de igualdad. Estableces una secuencia binaria (como por ejemplo hacemos con ASCII) para el operador "=". Para diferenciar los operadores de los dígitos binarios, puedes hacer que sean más cortos por ejemplo. Y lo explicas con casos "1=1", "2=2"... Puedes pasar al operador suma y explicarlo poniendo casos como "1+1=2", "1+2=3"... Así entenderían los que significa el "+". Luego pasas a la resta, multiplicación, etc. También serán útiles los operadores lógicos: AND, OR, NOT, etc... Lo mismo: poniendo ejemplos: "1 AND 1 = 1", "1 AND 0 = 0", etc...
El paso de la matemática abstracta a la física es más peliagudo, pero supongo que puedes recurrir a constantes matemáticas y físicas para que entiendan de qué estás hablando. La propia duración y longitud de onda de tu mensaje puede servirte de unidad de medida de tiempo y espacio. Si les mandas la velocidad de la luz, que es universal, expresada en esas unidades y usando el código numérico que ya les has explicado, se les hará el culo pepsicola.
Y así, poco a poco, escribes un manual de idioma "terrestre" y te dedicas a enviarlo en las frecuencias que tengan más posibilidades de llegar lejos con una potencia razonable.
La IA te da una respuesta, pero no un razonamiento, de esta manera nos podemos encontrar con la situación de "La guía del autoestopista intergaláctico"
Las matemáticas es el lenguaje universal. Si un día la civilización humana se encuentra con algún extraterrestre inteligente tendría que emplear las matemáticas para intentar comunicarse con él... luego el alienígena responderá con un rayo gamma o algo así.
#15 Yo coincido con #7. Por muy diferente que sea la tecnología, la cultura y la propia biología de los extraterrestres, sus matemáticas básicas deben ser iguales a las nuestras. Luego puede que hayan desarrollado unas áreas más que otras de forma diferente a nosotros, por sus circunstancias, pero lo elemental debe ser idéntico. Y a partir de ahí, ya tenemos una base común para empezar a comunicarnos.
Por ejemplo, si queremos enviar una señal inequívocamente artificial, podríamos emitir series de pulsos con los números primos: 2 pulsos, 3 pulsos, 5, 7, 11... Ningún fenómeno natural producirá una señal así. Una respuesta inequívocamente artificial podría ser que nos envíen la misma serie invertida, o el número siguiente al último que enviemos, etc. Una vez establecido que somos dos especies inteligentes, podríamos compartir códigos para estos números. Y después las operaciones matemáticas. Después las constantes físicas fundamentales. Después la química, basándonos en los números atómicos de los elementos. Astronomía, dónde estamos, cómo somos, etc... Paso a paso, podríamos elaborar un lenguaje común para llegar a entendernos sobre todo o casi todo.
Comentarios
Pues que, al igual que los humanos, no pueden encontrar la prueba de todo enunciado matemático cierto porque es un problema no computable. Es más, hay enunciados matemáticos ciertos que ningún teorema puede demostrar: https://es.wikipedia.org/wiki/Teoremas_de_incompletitud_de_G%C3%B6del
#6 Podrías explicarlo para mortales?
#10 Puedo intentarlo yo? Desconozco tu punto de partida así que disculpa si te parece demasiado simplificado o demasiado impreciso (pero correcto en lo esencial). Imagina un cuerpo axiomático no trivial. Imagina esto simplemente como un conjunto de enunciados (axiomas) de los que puedes extraer conclusiones lógicas (si fuese trivial, no podrías). Es decir, crear nuevos enunciados a partir de los ya existentes.
Por ejemplo, empiezas con: "0 es un número natural", "todo número natural tiene un sucesor que también es un número natural"... y otros... Entonces, a partir de la afirmación de que existe un sucesor, por ejemplo, puedes "deducir" (y demostrar dentro del contexto que has establecido) que existe la suma, expresarlo formalmente, y seguir construyendo la aritmética, por ejemplo.
Lo que viene a decir esto es que no existe teoría alguna en la que no existan ciertos enunciados posibles que no se pueden demostrar de ningún modo a partir de los ya existentes. Siempre puedes buscar alguno que es indecidible. Esto quiere decir que las combinaciones de los enunciados que ya tienes no te permiten deducir si el nuevo es cierto o no.
La solución es añadir un nuevo axioma que decida ese caso que sea consistente con todos los demás (básicamente estás diciendo "este caso que no estaba resuelto es así por esta nueva información que no contradice nada de lo otro"), pero el resultado (consecuencia de los teoremas de incompletitud) será que, añadiendo un enunciado nuevo, estás engendrando aún más posibilidades de nuevos enunciados que son indemostrables a menos que añadas nuevos axiomas a su vez. Y, cuando añades nuevos enunciados, los nuevos enunciados indemostrables posibles crecen a un ritmo aún más rápido. De modo que, cualquier construcción de una teoría matemática autoconsistente que puedas llevar a cabo, estará siempre (y cada vez más) incompleta.
#12 Mañana me lo leo con más calma. Pero muchas gracias.
No veo que los ordenadores estén a día de hoy escribiendo pruebas.
#3 https://en.wikipedia.org/wiki/Computer-assisted_proof
Existen lenguajes lógicos orientados exclusivamente a esto, por ejemplo: https://coq.inria.fr/
#21 Sí, es un lenguaje. Entonces una persona lo utilizará para manejar las máquinas.
Estamos ante una herramienta.
#23 Bueno, genera pruebas de forma automática a problemas que son descritos en ese lenguaje.
De hecho, basándose en la fuerza bruta, en la teoría, es muy fácil generar pruebas de forma automática si tratas un cuerpo axiomático como un lenguaje regular. Sólo tienes que generar todas las combinaciones posibles para ir generando todos los teoremas posibles junto con sus pruebas. Otra cuestión es que la mayor parte de los resultados sean inútiles, y nunca se acaban...
#25 si eso valiera para algo, se habría estado usando desde la antigua Grecia.
Alguien tendrá que comprobar que las pruebas son correctas.
#1 Me temo que en 10 o 20 años cada vez menos matematicos van a ser capaces de refutar o validar las pruebas sin ayuda de otras computadoras.
Dicho esto, creo que la pareja humano-maquina sera como se innove por muchos años. Viene pasando en el ajedrez y ya hacen mas de 30 años que Deep Blue ganos sobre a los humanos
#2 es como decir que los carpinteros no pueden hacer muebles sin ayuda de una sierra. Si es un instrumento, es un instrumento, nada más.
#4 un carpintero puede hacer un mueble sin herramientas, partiendo de un tronco de madera en bruto, y que le quede igual que con las herramientas?
#18 A ver, que no es ese el tema. El tema es que a día de hoy, para avanzar las matemáticas hacen falta personas.
#2
Pienso lo mismo. Para mí el problema llegará cuando la máquina escriba proposiciones que no podamos seguir, que podamos comprobar que son correctas pero, o bien no seamos capaces de seguir la secuencia deductiva que lleva a la máquina a hacer una afirmación, o no podamos seguir la demostración matemática (esto parece menos probable). Pero sobre todo cuando la máquina simplemente 'lo sepa' y no podamos saber por qué.
#2 al igual que en otras muchas materias, hace décadas que en física nadie es capaz de refutar nada sin un acelerador de partículas, por ejemplo ¿Porqué las matemáticas iban a ser diferentes?
#8 Porque la física es experimental al ser modelos que tratar de parametrizar la realidad. Las matemáticas no. La física teórica solo es teoría hasta que se refuta experimentalmente.
#9 Y para eso a veces hacen falta herramientas
#20 En una determinada frecuencia, puedes empezar enviando secuencias de pulsos según los números primos: dos pulsos, tres pulsos, cinco pulsos... "pip-pip pip-pip-pip ..." Esto despertaría la curiosidad de cualquier observador.
A continuación (después de llegar a 1009 por ejemplo), explicas que vas a usar la numeración binaria: mandas un pulso seguido de 000001 pulsos (siendo 0 un lapso sin pulso que dure lo mismo que el pulso), mandas dos pulsos seguidos de 000010,... y así sucesivamente. La longitud de tus bytes (6 bits en este ejemplo) es arbitraria.
Lo siguiente es explicar los conceptos matemáticos y lógicos básicos. El primero es el operador de igualdad. Estableces una secuencia binaria (como por ejemplo hacemos con ASCII) para el operador "=". Para diferenciar los operadores de los dígitos binarios, puedes hacer que sean más cortos por ejemplo. Y lo explicas con casos "1=1", "2=2"... Puedes pasar al operador suma y explicarlo poniendo casos como "1+1=2", "1+2=3"... Así entenderían los que significa el "+". Luego pasas a la resta, multiplicación, etc. También serán útiles los operadores lógicos: AND, OR, NOT, etc... Lo mismo: poniendo ejemplos: "1 AND 1 = 1", "1 AND 0 = 0", etc...
El paso de la matemática abstracta a la física es más peliagudo, pero supongo que puedes recurrir a constantes matemáticas y físicas para que entiendan de qué estás hablando. La propia duración y longitud de onda de tu mensaje puede servirte de unidad de medida de tiempo y espacio. Si les mandas la velocidad de la luz, que es universal, expresada en esas unidades y usando el código numérico que ya les has explicado, se les hará el culo pepsicola.
Y así, poco a poco, escribes un manual de idioma "terrestre" y te dedicas a enviarlo en las frecuencias que tengan más posibilidades de llegar lejos con una potencia razonable.
Y a esperar.
Si tan listas son, que demuestren o refuten la Conjetura de Collatz, que me da curiosidad.
La IA te da una respuesta, pero no un razonamiento, de esta manera nos podemos encontrar con la situación de "La guía del autoestopista intergaláctico"
Las matemáticas es el lenguaje universal. Si un día la civilización humana se encuentra con algún extraterrestre inteligente tendría que emplear las matemáticas para intentar comunicarse con él... luego el alienígena responderá con un rayo gamma o algo así.
#7 >> luego el alienígena responderá con un rayo gamma
Por eso hay que estar callados ... no vayamos a estar en el bosque oscuro.
https://es.wikipedia.org/wiki/Hip%C3%B3tesis_del_bosque_oscuro
#7 "Las matemáticas es el lenguaje universal." ¿Podría elaborar un poco este enunciado? Gracias.
#15 Yo coincido con #7. Por muy diferente que sea la tecnología, la cultura y la propia biología de los extraterrestres, sus matemáticas básicas deben ser iguales a las nuestras. Luego puede que hayan desarrollado unas áreas más que otras de forma diferente a nosotros, por sus circunstancias, pero lo elemental debe ser idéntico. Y a partir de ahí, ya tenemos una base común para empezar a comunicarnos.
Por ejemplo, si queremos enviar una señal inequívocamente artificial, podríamos emitir series de pulsos con los números primos: 2 pulsos, 3 pulsos, 5, 7, 11... Ningún fenómeno natural producirá una señal así. Una respuesta inequívocamente artificial podría ser que nos envíen la misma serie invertida, o el número siguiente al último que enviemos, etc. Una vez establecido que somos dos especies inteligentes, podríamos compartir códigos para estos números. Y después las operaciones matemáticas. Después las constantes físicas fundamentales. Después la química, basándonos en los números atómicos de los elementos. Astronomía, dónde estamos, cómo somos, etc... Paso a paso, podríamos elaborar un lenguaje común para llegar a entendernos sobre todo o casi todo.
#16 La cuestión es pasar de esa "base" a la comunicación, es decir, del símbolo "una serie de pulsos con los números primos" al significado.