Indique a afirmación. O núcleo decide se é probada.

Un panel de modelos ataca o problema coa literatura, SageMath, PARI/GP e un solucionador SMT, e logo formaliza o resultado en Lean 4 contra Mathlib. O núcleo de Lean ou acepta a proba ou non, e non hai cantidade de prosa segura que cambie iso. Cando falla, obtén o obxectivo exacto que queda, que é normalmente onde o argumento informal era acenar coa man.

O obxectivo
Sexa específico acerca do que significa feito. 'Decidir se X é verdadeiro e demostralo' é mellor que 'Contarme sobre X'.
A barra que ten que limpar
O árbitro sostén literalmente esta barra. Pídalle unha proba de nivel de premio e dirá claramente cando o panel cae, en lugar de declarar a vitoria.
O panel
Máis asentos significan máis ángulos, e máis custo por rolda.
Árbitro
Regras sobre os criterios e comproba cada proba, vale o teu modelo máis forte.
Rondas
Límite de gasto
Se o golpeas, a partida pausa. Non se perde nada.
Visibilidade
Inscríbase para comezar unha partida
As contas novas reciben crédito inicial, suficiente para unha partida real.
Un verificador que non se pode convencer

Lean 4 con Mathlib comproba o tipo da declaración final, e unha proba que se basea en sorry, native_decide ou un axioma novo é rexeitada en vez de contada. Xunto a ela: SageMath, PARI/GP, Z3, CVC5 e o OEIS, de xeito que unha construción pode ser calculada e identificada antes de que alguén tente probar algo sobre ela.

Unha proba fracasada é un achado

Cando a formalización falla, o obxectivo que Lean non puido cumprir é entregado a calquera sitio que estea mellor situado para atacar: só ese obxectivo, non toda a historia. Unha proba rexeitada nomea a lacuna precisamente, o que é máis do que a maioría dos argumentos informais nunca fan.

Nada se proba dúas veces.

Cada lema que o panel estabelece vai nun libro compartido coa súa proba, polo que nunca se deriva de novo e nunca se tentan de novo os puntos mortos. Os problemas longos pausan e reanúdanse sen perder o traballo: pecha a páxina e volta mañá.