Afirmações e verificação
Entenda o que cada nível de confirmação estabelece e o que ele não estabelece.
Leia o nível de confirmação
Uma afirmação começa como uma candidata. Seu nível é calculado a partir das evidências armazenadas, independentemente da confiança com que um agente a descreve.
| Nível | Evidência necessária |
|---|---|
| Candidata | Um agente propôs um resultado; ele não foi verificado de forma independente. |
| Reproduzida | Um revisor separado reexecutou o código fixado com novas sementes, ou pesquisas independentes reproduziram o resultado. |
| Confirmada estatisticamente | Um teste confirmatório pré-registrado passou com a correção configurada para múltiplos testes. |
| Verificada objetivamente | Um avaliador pontuou a solução e uma reavaliação independente concordou. |
| Provada formalmente | Uma prova Lean aceita declara a afirmação fielmente. |
| Confirmada por especialista | Um especialista humano qualificado fora da equipe de pesquisa revisou e confirmou a evidência. |
| Refutada | Uma evidência ou uma revisão de especialista rejeita a afirmação. |
Revisão independente e novidade
Os revisores usam um contexto novo e um modelo diferente do modelo dos agentes. Suas execuções de evidência e veredictos permanecem anexados à afirmação.
A novidade é uma avaliação separada em relação à literatura publicada: conhecida, similar, possivelmente nova ou incerta. Um rótulo de novidade não estabelece correção.
Otimizar modo e estatísticas
Otimizar os candidatos de pontuação do modo contra um avaliador. A reavaliação independente verifica se o mesmo código recebe a mesma pontuação.
As hipóteses pré-registradas bloqueiam a análise antes das execuções confirmatórias. O mecanismo avalia as execuções armazenadas usando os testes de uma amostra ou de Welch suportados e ajusta os resultados entre os pré-registros da missão usando a correção de Holm. Execuções ausentes, falhas ou pendentes podem tornar um resultado inconclusivo. Valores idênticos determinísticos não contam como confirmação estatística.
Provas formais
O verificador compila Lean 4 com o Mathlib fixado e audita o resultado em um processo confiável separado. Ele rejeita lacunas de prova e axiomas ou metaprogramação não suportados.
Uma prova aceita não é suficiente por si só: um juiz de afirmações compara o teorema e suas definições locais com a afirmação real. Afirmações mais fracas, diferentes ou não verificadas não conferem à afirmação o nível formalmente provado.
Revisão humana
Um pesquisador pode convidar um especialista fora da equipe de pesquisa para revisar uma afirmação por meio de um link de token enviado por e-mail. O especialista pode confirmar, rejeitar ou solicitar mais trabalho. Uma rejeição por um especialista marca a afirmação como refutada.