Indicar la reclamación. El núcleo decide si se prueba.
Un panel de modelos ataca su problema con la literatura, SageMath, PARI/GP y un solucionador SMT, luego formaliza el resultado en Lean 4 contra Mathlib. El núcleo de Lean acepta la prueba o no, y ninguna cantidad de prosa segura cambia eso. Cuando falla, obtiene el objetivo exacto que queda, que es generalmente donde el argumento informal era la agitación de manos.
Un verificador que no puede ser persuadido
Lean 4 con Mathlib tipo-chequea la declaración final, y una prueba que se apoya en sorry, native_decide o un axioma fresco se rechaza en lugar de contar. Junto a ella: SageMath, PARI/GP, Z3, CVC5 y el OEIS, por lo que una construcción puede ser computada e identificada antes de que alguien intente probar nada al respecto.
Una prueba fallida es un hallazgo
Cuando la formalización falla, el objetivo que Lean no pudo cerrar se entrega a cualquier asiento que esté mejor situado para atacarlo: sólo ese objetivo, no toda la historia. Una prueba rechazada nombra la brecha precisamente, que es más que la mayoría de los argumentos informales jamás lo hacen.
Nada se prueba dos veces
Cada lema que establece el panel va en un libro mayor compartido con su prueba, por lo que nunca se vuelve a derivar y los callejones sin salida nunca se vuelven a juzgar. Los problemas largos se pausan y se reanudan sin perder trabajo: cierra la pestaña y vuelve mañana.