La IA ya demuestra teoremas: el peligro de formalizar todas las matemáticas a toda prisa
How to Formalize All of Mathematics
Un grupo de expertos en formalización matemática celebra los avances de la IA para demostrar teoremas, pero advierte que los llamados a formalizar todo el conocimiento matemático lo más rápido posible podrían causar un daño duradero. Recuerdan el caso de Math, Inc., que generó código que hubo que descartar por completo, y defienden un esfuerzo coordinado y bien hecho que haga florecer las matemáticas.
Si se hace bien, un esfuerzo de formalización coordinado a gran escala podría ampliar enormemente la exploración y el descubrimiento matemáticos. Si se hace mal, será, en el mejor de los casos, un desperdicio de recursos; lo más probable es que cause un daño duradero.