Afirmaciones y verificación
Comprende qué establece cada nivel de confirmación y qué es lo que no establece.
Lee el nivel de confirmación
Una afirmación comienza como candidata. Su nivel se calcula a partir de la evidencia almacenada, independientemente de la confianza con la que un agente la describa.
| Nivel | Evidencia requerida |
|---|---|
| Candidata | Un agente ha propuesto un resultado; no ha sido verificado de forma independiente. |
| Reproducida | Un revisor separado volvió a ejecutar el código fijado con nuevas semillas, o investigaciones independientes reprodujeron el resultado. |
| Confirmada estadísticamente | Una prueba confirmatoria prerregistrada pasó con la corrección configurada para múltiples pruebas. |
| Verificada objetivamente | Un evaluador puntuó la solución y una reevaluación independiente coincidió. |
| Probada formalmente | Una prueba Lean aceptada establece fielmente la afirmación. |
| Confirmada por experto | Un experto humano elegible fuera del equipo de investigación revisó y confirmó la evidencia. |
| Refutada | La evidencia o una revisión de un experto rechazan la afirmación. |
Revisión independiente y novedad
Los revisores utilizan un contexto fresco y un modelo diferente al modelo de los agentes. Sus ejecuciones de evidencia y veredictos permanecen vinculados a la afirmación.
La novedad es una evaluación separada frente a la literatura publicada: conocida, similar, posiblemente nueva o incierta. Una etiqueta de novedad no establece la corrección.
Modo de optimización y estadísticas
Optimiza las puntuaciones de los candidatos de modo frente a un evaluador. Una reevaluación independiente verifica si el mismo código recibe la misma puntuación.
Las hipótesis prerregistradas bloquean el análisis antes de las ejecuciones confirmatorias. El motor evalúa las ejecuciones almacenadas utilizando las pruebas de una muestra o de Welch compatibles y realiza ajustes en todas las prerregistraciones de la misión mediante la corrección de Holm. Las ejecuciones faltantes, fallidas o pendientes pueden hacer que un resultado no sea concluyente. Los valores idénticos deterministas no cuentan como confirmación estadística.
Pruebas formales
El verificador compila Lean 4 con el Mathlib fijado y audita el resultado en un proceso de confianza separado. Rechaza brechas de prueba y axiomas o metaprogramación no compatibles.
Una prueba aceptada no es suficiente por sí sola: un juez de enunciados compara el teorema y sus definiciones locales con la afirmación real. Los enunciados más débiles, diferentes o no verificados no otorgan a la afirmación el nivel de formalmente probado.
Revisión humana
Un investigador puede invitar a un experto ajeno al equipo de investigación para que revise una afirmación a través de un enlace de token enviado por correo electrónico. El experto puede confirmar, rechazar o solicitar más trabajo. El rechazo de un experto marca la afirmación como refutada.