Distinguir este punto es un problema central en matemáticas a la hora de aceptar demostraciones computacionales de un problema.
Exagerando, supongamos que logro demostrar la hipótesis de Riemann usando el Matlab o el Maple para hacer determinados pasos de la demostración (podrían ser integrales incalculables a mano, sumar series, o incluso manipular expresiones simbólicas).
Para muchos, esta demostración no sería válida: estos programas no son gratuitos ni open source, con lo cual no estaría a disposición de cualquiera chequear que no haya errores en la parte computacional de la demostración.
La parte más difícil de verificar es la que se debe al código del programa: ¿qué algoritmos usa para resolver lo que le pedimos? Si bien suelen estar documentados ('emplea un runge-kutta blablabla...'), no sabemos cómo están implementados, cómo funcionan internamente. ¿Cómo saber que no hay errores, que un algoritmo no tiene alguna falla?
Este es el principal argumento contra la demostración de la conjetura de Kepler que va a salir en el Annals del que hablábamos en el post de las
El solo cálculo de π o de √2 involucra -en esta clase de programas- el uso de cajas negras, que tiran una lista de cifras en las cuales tenemos que 'creer'. Por ese motivo, T.Hales está trabajando en una nueva demostración en el Flyspeck Project, y le calculan unos veinte años... Uno puede unirse al grupo, si está interesado.
In Mathematica, it is also possible to write a procedure whose input is n and whose output is a rational number x such that abs(pi-x) < 10^-n. However, the Mathematica procedure ApproxPi[n_]:=Rationalize[N[Pi,n+1],10^-n] relies on algorithms that are unknown origin and unknown reliability. What does N[Pi,n+1] do behind the scenes? How reliable is it? Can you prove this line of code always does what you wanted? Or do you detect a subtle bug?
1 comentario:
Citado en la pagina del Flyspeck:
Fejes Tóth thinks that this situation will occur more and more often in mathematics. He says it is similar to the situation in experimental science - other scientists acting as referees can't certify the correctness of an experiment, they can only subject the paper to consistency checks. He thinks that the mathematical community will have to get used to this state of affairs.
(Fejes Tóth fue el jefe del grupo de referis del paper). Es escalofriante pensar que uno esta viviendo una revolucion en la concepcion de una ciencia milenaria. Es casi como ver, en vivo, el fin de los dinosaurios; o el surgimiento del Himalaya.
Escrito por Matias a las Marzo 22, 2004 11:21 AM
lástima que acá los dinosaurios vamos a ser nosotros ;)
¿viste el manifiesto que linkean? Leibniz estaría orgulloso...
Escrito por JuanPablo a las Marzo 22, 2004 12:05 PM
Algo similar pasó con la demostración del problema de coloreo de grafos.
Se quería demostrar que para colorear cualquier mapa (sin que dos países limítrofes tengan el mismo color) alcanzaban 4 colores (durante muchos años se pensó que eran cinco). No me acuerdo los apellidos de las personas que lo lograron pero para eso tuvieron que agrupar los estilos de mapas y con un programa de computación demostraron que con 4 bastaba.
Creo que fue el primer caso de demostraciones con computadoras. En su momento hubo mucha controversia al respecto.
Escrito por Jonathan a las Marzo 22, 2004 12:07 PM
no se, la verdad no soy ningun experto en el tema, ni parecido. pero me imagino que debe de haber metodos para "chequear" algoritmos. onda esas cosas que se prueban para un caso, entonces vale para este otro y asi sucesivamente (induccion?).
Escrito por sascuatsh a las Marzo 22, 2004 10:22 PM
El problema no es si es posible chequear los algoritmos, sino que los dos programas de manipulación simbólica y "cuentas" más exitosos y difundidos, el Mathematica (de Urbana, Illinois) y el Maple (de Waterloo, Ontario), no hacen públicos sus algoritmos. No solo eso, sino que los defienden con uñas y dientes, y entonces un referí no tiene acceso a información vital para verificar la validez de un paper hecho con esas herramientas.
Dicho sea de paso, el Mathematica me viene bárbaro para chequear que hice bien las integrales triples antes de ponerlas en las soluciones de las prácticas ! Y se la bancaba muy bien el semestre pasado con las transformadas de Laplace.
Escrito por Martín a las Marzo 23, 2004 02:15 AM
lo que dice martin es el punto clave para poder chequear los algoritmos: mientras el programa no sea de fuente abierta, no tenemos forma de averiguar qué está haciendo.
(yo prefiero el matlab, pero al nivel que lo uso, no tiene ninguna ventaja con los otros)
Escrito por JuanPablo a las Marzo 23, 2004 12:09 PM
Es cierto que el hecho de que parte de los algoritmos sea publico o no lo sea, cambia mucho las cosas. Pero esto no es todo el problema, al menos en este caso. Creo que Hales no uso ningun programa cerrado, o al menos no fue este el punto. El punto fue que para los referis, chequear todo el paper fue casi imposible. Hubo un grupo de referis, que se tomaron un laburo absolutamente fuera de lo comun: hicieron seminarios para entender partes de la demostracion. Chequeaban cada cuenta, y aquellas afirmaciones que no estaban escritas en profundidad, las desarrollaban hasta ver que realmente eran ciertas (eso les llevaba dias a veces). Pero no pudieron con todo.
Muchos papers en matematica, si no todos, se publican sin que los referis hayan revisado exhaustivamente todo el contenido. Este era una excepcion, justamente porque el problema era excepcional. Si bien todo el mundo pensaba que la conjetura era cierta, se trataba justamente de dar una demostracion.
Sugiero seguir el link que pone JuanPablo. Uno se entera que hay proyectos para terminar con estas cosas. Esta el manifiesto QED, y tiene sus versiones en computadora (CAML, por ejemplo). La idea es hacer un entorno, abierto, donde los teoremas se puedan chequear. Donde la logica se pueda mirar hasta las ultimas consecuencias. Suponen los autores que si en el futuro alguien es capaz de crear un "teorema" con estos lenguajes, el propio entorno ya lo chequeo, y todos pueden estar seguros de que es valido. Es realmente cambiar mucho en la forma de hacer matematica.
Escrito por Matias a las Marzo 23, 2004 02:49 PM
igual, que sean abiertos o no es un punto que el propio Hales resalta, en el párrafo que copié sobre pi.
Escrito por JuanPablo a las Marzo 23, 2004 03:10 PM
Si, claro, el que sean abiertos es importante. Pero no estoy seguro de que sea el meollo de la cosa.
Yo recien me topo con estos programas/lenguajes, aun estoy tratando de entender "con que se comen". De hecho, en mi comentario anterior debi haber escrito HOL donde puse CAML (este ultimo es el lenguaje en el que esta escrito el HOL, segun entiendo ahora). Y es mi desconocimiento tal vez el que me lleva a aventurar que esto es una revolucion en matematica. O mi necesidad de ver que algo en matematica debe cambiar. JuanPablo: como era lo del espectro? ;-)
Escrito por Matias a las Marzo 24, 2004 10:38 AM
¿vos preguntás por ésto? ;-)
Escrito por JuanPablo a las Marzo 24, 2004 11:31 AM
Si, por eso! Yo vi "Sexto sentido" y ahi te explican todo.
Escrito por Matias a las Marzo 25, 2004 01:01 PM
Matías, es verdad que muchas veces los referís no chequean exhaustivamente el contenido.
Pero hay que balancear las cosas: primero, que muchas veces sí chequean todo el contenido hasta el final. Por otra parte, cuando un paper importante llega hasta el referí, normalmente el autor ya ha contado eso en un montón de seminarios, y todos los especialistas lo conocen. El referí tiene en cuenta también la experiencia y nivel del autor. Aún así pasa que se publican demostraciones erróneas. Pero lo interesante es que casi no hay casos de resultados falsos: aún en los casos (algunos importantes) en que se ha publicado una demostración errónea, el teorema sí es cierto y se hace un demostración correcta más tarde.
También conozco el caso inverso, un paper sobre un resultado importante, rechazado porque el referí no logra convencerse de que la demostración está bien. Y después, tras un seminario de meses, el autor finalmente logra hacer entender la demostración a otros matemáticos.
Escrito por Martín a las Marzo 26, 2004 10:16 AM
Con el anteúltimo mío pasó algo raro. Dos años dando vueltas, porque el resultado era bueno pero faltaba un punto clave de la demostración... que estaba demostrado desde la década del sesenta!!
Escrito por JuanPablo a las Marzo 26, 2004 03:47 PM
Es que es imposible pedirle a alguien hoy en dia que conozca todos los resultados de su area; salvo unos pocos elegidos, la gran mayoria conoce(mos) una infima parte de lo que esta hecho. Por eso un "verificador automatico", donde la comunidad matematica pueda poner "toda la matematica", seria un paso sustancialmente distinto a lo que hoy se estila.
Escrito por Matias a las Marzo 26, 2004 07:17 PM
Yo pienso que muchas veces los matemáticos son demasiado desconfiados. Si se demuestra algo con Matlab, se hace la prueba también con Mathematica y Maple a ver si los resultados son los mismos. ¿No sería mucha casualidad que los tres programas tuvieran el mismo bug?
Escrito por ToReK a las Marzo 27, 2004 05:39 AM
hay dos respuestas para eso:
la primera, que en matemáticas no se acepta que algo sea 'improbable', tiene que ser 'imposible'.
Mientras haya una chance de que los programas estén fallando, y no pueda demostrarse que no, estamos en la categoría 'improbable'.
Escrito por JuanPablo a las Marzo 27, 2004 10:37 AM
la segunda, es que los tres programas son diferentes, y se comportan distinto ante problemas iguales.
Con el maple se puede hacer manipulación simbólica ('despeja letras' en las ecuaciones o funciones, podríamos decir). El matlab (matrix-laboratory) no lo hace pero es excelente en trabajo matricial: se pueden hacer cuentas con matrices gigantes.
Pese a todo, el matlab invierte la matriz [1 2 3, 4 5 6, 7 8 9], que no es inversible...
Escrito por JuanPablo a las Marzo 27, 2004 10:45 AM
Y cuál es la "inversa" ?
Escrito por Martín a las Marzo 30, 2004 11:49 PM
Un comentario, un poco al margen (o no). Juan Pablo dice "en matematicas no se acepta que algo sea improbable". Si bien esto es rigurosamente cierto, tambien es cierto que para los matematicos el nivel de "improbabilidad" cambia un poco las cosas. Para poner un caso extremo, posiblemente el problema mas importante hoy en dia a resolver es la hipotesis de Riemmann. Si bien hoy esta al nivel de una conjetura, pues no fue probada, hay mucho trabajo de gente que empieza con "si la hipotesis de Riemmann es verdadera, entonces se puede probar que.....".
Es decir, para muchos matematicos vale la pena invertir tiempo en intentar probar resultados suponiendo que la hipotesis de Riemmann es verdadera, porque estan convencidos de que, tarde o temprano, alguien demostrara que lo es. Nadie piensa que pueda no serlo, aunque siga siendo una conjetura.
Escrito por Matias a las Marzo 31, 2004 12:40 PM
ok, pero me refiero a la hora de dar algo por demostrado, no a la hora de darle usos.Uno simplemente puede trabajar dejando en claro que hay un hueco en la demostración.
Como en el caso de las esferas, que en las fruterías apilan las manzanas como dice Hales que es óptimo, aunque no lo tengan demostrado ;)
Escrito por JuanPablo a las Marzo 31, 2004 04:59 PM
Martin, da:
1.0 e+16 * [-0,45 0,90 -0,45; 0,90 -1,80 0,90; -0,45 0,90 -0,45] (con doble precisión, conseguís una bocha de decimales, pero empiezan igual)
la matriz es [a b a; b c b; a b a], simétrica, y si uno ahora hace a.b da [2 0 0; 8 0 -4; 16 0 8]
y si se hace b.a=[0 -4 0; 0 8 0; 4 0 0]
Escrito por JuanPablo a las Marzo 31, 2004 05:07 PM
Publicar un comentario