Un proyecto de investigación ha logrado automatizar una porción significativa de la topología general, un campo complejo de las matemáticas, utilizando modelos de lenguaje grandes (LLMs). Según un estudio publicado en arXiv el 6 de enero de 2026, el equipo liderado por Josef Urban ha formalizado aproximadamente 130,000 líneas de código en dos semanas, desde el 22 de diciembre hasta el 4 de enero, con un costo de suscripción de aproximadamente 100 dólares para el LLM. Este proceso, que comenzó en noviembre de 2025, involucra un bucle de retroalimentación entre un LLM (principalmente ChatGPT 5.2 o Claude Sonnet 4.5) y un verificador de pruebas, utilizando bibliotecas de formalización existentes. Entre los logros del proyecto se incluyen la formalización de lemmas y teoremas clave, como el lemma de Urysohn y el teorema de metrización de Urysohn. Los investigadores creen que esta metodología simple y económica podría democratizar la formalización matemática, haciéndola accesible a un público más amplio y potencialmente ubicua en 2026, independientemente del asistente de pruebas utilizado. El estudio destaca el potencial de la IA para acelerar y simplificar tareas complejas en campos técnicos.
Noticias agregadas con IA