¿Estamos atrapados con Lean? El debate sobre alternativas en asistentes de prueba
Are We Stuck with Lean?
Pregunto si la comunidad matemática tiene perspectivas reales para apoyar una alternativa a Lean, sugiriendo Metamath por su mayor garantía de corrección y base en teoría de conjuntos. Reconozco que la popularidad de Lean se debe en parte a su comunidad y a Mathlib, pero creo que los avances en IA podrían hacer viable construir bibliotecas similares para otros asistentes de prueba, ofreciendo así opciones más sólidas.
Estoy preocupado de que gran parte de la popularidad de Lean se deba a que unas pocas personas prominentes lo eligieron y le dieron un alto perfil, no necesariamente porque sea objetivamente el mejor asistente de prueba para el trabajo que queremos hacer.