La comunidad matemática debate si la adopción masiva de Lean como asistente de demostración interactiva (ITP) ha llegado a un punto de no retorno o si aún es viable apoyar una alternativa con base en teoría de conjuntos. El autor recuerda que hace tres años Lean ya acumulaba impulso gracias al Proyecto Xena de Kevin Buzzard y al experimento Liquid Tensor de Peter Scholze, pero aún quedaban incertidumbres: Terry Tao no había aprendido Lean y la migración de Mathlib a la versión 4 se había completado apenas.
La pieza sostiene que la popularidad de Lean responde en parte al respaldo de figuras influyentes, no necesariamente a superioridad técnica objetiva, y señala dos argumentos a favor de explorar alternativas como Metamath, Mizar o Isabelle/ZF. Primero, Metamath contaría con el trabajo de Mario Carneiro sobre Metamath Zero, que ofrecería mayores garantías de corrección formal, algo relevante porque Lean no es inmune a errores de solidez. Segundo, al basarse en teoría de conjuntos, evitaría las objeciones filosóficas a la doctrina proposiciones-como-tipos defendida por James Hanson en MathOverflow.
La principal fortaleza de Lean es Mathlib, una biblioteca enorme cuya réplica parecía inviable. El autor argumenta que los avances en inteligencia artificial para escribir matemáticas formales podrían hacerla concebible. Aunque no propone abandonar Lean ni cuestiona la calidad de su comunidad, defiende que un ITP alternativo viable beneficiaría a la comunidad matemática y requiere apoyo institucional que hoy no está claro de dónde provendría.