El medallista Fields Peter Scholze (Universität Bonn) anunciaba recientemente en el blog de Kevin Buzzard (Imperial College London) que, tras medio año, se habían alcanzado éxitos significativos en el reto Liquid Tensor Experiment que había propuesto a la comunidad de entusiastas de las demostraciones asistidas por ordenador articulado alrededor del Lean Prover Zulip Chat. Scholze afirma que le “parece una absoluta locura que los asistentes de prueba interactivos se encuentren ahora en el nivel en el que, en un lapso de tiempo muy razonable, puedan verificar formalmente una investigación original difícil”.
El reto consistía en formalizar para el Lean Proof Assistant un resultado, con una demostración particularmente enrevesada, de las Lectures on Analytic Geometry, texto en el que P. Scholze y Dustin Clausen (University of Copenhagen) están desarrollando bajo el nombre de condensed mathematics un novedoso proyecto de unificación de diferentes teorías matemáticas. El desafío de Scholze fue aceptado entusiastamente por la comunidad de Lean, en particular por Kevin Buzzard, quien hablará como conferencista invitado en el ICM 2022 sobre los avances de los asistentes de demostraciones, de Johan Commelin (Universität Freiburg) y de Patrick Massott (Université Paris-Saclay). Se puede leer más acerca de esta historia en el artículo Mathematicians welcome computer-assisted proof in ‘grand unification’ theory de Davide Castelvecchi publicado en Nature el 18 de junio. Con respecto a la teoría de condensed mathematics recomendamos este reciente hilo de tweets de Laurent Fargues (Institut de mathématiques de Jussieu – Paris).
Mapa de la formalización en Lean de la noción de espacio perfectoide.
