Cuando las computadoras escriben pruebas, ¿qué sentido tienen los matemáticos? [EN]

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.

[#1 Chuache_cientifico]

Alguien tendrá que comprobar que las pruebas son correctas.

[#2 JungSpinoza]

#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

[#5 DerTeufel]

#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é.

[#4 --731452--]

#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.

[#18 Qwerty1234]

#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?

[#24 --731452--]

#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.

[#8 Varlak]

#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?

[#9 NanakiXIII]

#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.

[#19 Varlak]

#9 Y para eso a veces hacen falta herramientas

[#3 --731452--]

No veo que los ordenadores estén a día de hoy escribiendo pruebas.

[#21 Einwanderer]

#3 en.wikipedia.org/wiki/Computer-assisted_proof
Existen lenguajes lógicos orientados exclusivamente a esto, por ejemplo: coq.inria.fr/

[#23 --731452--]

#21 Sí, es un lenguaje. Entonces una persona lo utilizará para manejar las máquinas.
Estamos ante una herramienta.

[#25 Einwanderer]

#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...

[#26 --731452--]

#25 si eso valiera para algo, se habría estado usando desde la antigua Grecia.

[#6 gambader]

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: es.wikipedia.org/wiki/Teoremas_de_incompletitud_de_Gödel

[#10 Hjkk]

#6 Podrías explicarlo para mortales?

[#12 Einwanderer]

#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…   

[#13 Hjkk]

#12 Mañana me lo leo con más calma. Pero muchas gracias.

[#7 cocococo]

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í.

[#14 JungSpinoza]

#7 >> luego el alienígena responderá con un rayo gamma

Por eso hay que estar callados ... no vayamos a estar en el bosque oscuro.

es.wikipedia.org/wiki/Hipótesis_del_bosque_oscuro

[#16 ElPerroDeLosCinco]

#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…   

[#20 galton]

#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.

[#22 ElPerroDeLosCinco]

#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í…   

[#15 galton]

#7 "Las matemáticas es el lenguaje universal." ¿Podría elaborar un poco este enunciado? Gracias.

[#11 mcfgdbbn3]

Si tan listas son, que demuestren o refuten la Conjetura de Collatz, que me da curiosidad.

[#17 OniNoNeko_Levossian]

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"