Leyendo el tema, el algoritmo ha descubierto un teorema y una conjetura...
Es decir, no ha probado nada....
El teorema habría que verlo....
Más bien, el algoritmo
ha ayudado a
enunciar varias conjeturas... alguna de las cuales los autores han sido capaces de demostrar (de forma independiente, sin ayuda de ordenadores) y por tanto ahora son teoremas.
Pero la idea detrás es muy sencilla: se trata de encontrar relaciones (conjeturales) entre varios invariantes asociados a un objeto encontrando una función que prediga un invariante a partir de los demás (aquí se usa el ML, para ajustar la función empíricamente). Una vez tienes la función, puedes conjeturar que tal invariante es tal función de tales otros invariantes y en caso de que la conjetura sea cierta ya depende de tu habilidad como matemático ser capaz de demostrarla.
Pero vaya, sin querer quitarle mérito a esto, pues estoy seguro de que estas cosas van a ser cada vez más útiles y más utilizadas, de "demostrar teoremas" o de hacer cosas creativas de momento nada de nada.
