Affermazioni e verifica
Comprendi cosa stabilisce ogni livello di conferma e cosa non stabilisce.
Leggi il livello di conferma
Un'affermazione inizia come candidata. Il suo livello è calcolato dalle prove memorizzate, indipendentemente da quanto con sicurezza un agente la descriva.
| Livello | Prove richieste |
|---|---|
| Candidata | Un agente ha proposto un risultato; non è stato controllato indipendentemente. |
| Riproduzione | Un revisore separato ha rieseguito il codice fissato con nuovi seed, o ricerche indipendenti hanno riprodotto il risultato. |
| Confermata statisticamente | Un test di conferma preregistrato è passato con la correzione configurata per test multipli. |
| Verificata oggettivamente | Un valutatore ha assegnato un punteggio alla soluzione e una riconsiderazione indipendente ha concordato. |
| Provata formalmente | Una prova Lean accettata dichiara fedelmente l'affermazione. |
| Confermata da esperti | Un esperto umano idoneo esterno al team di ricerca ha esaminato e confermato le prove. |
| Confutata | Una prova o una revisione di un esperto rifiuta l'affermazione. |
Revisione indipendente e novità
I revisori utilizzano un contesto fresco e un modello diverso dal modello degli agenti. Le loro prove, esecuzioni e verdetti rimangono collegati all'affermazione.
La novità è una valutazione separata rispetto alla letteratura pubblicata: nota, simile, potenzialmente nuova o poco chiara. Un'etichetta di novità non stabilisce la correttezza.
Ottimizza modalità e statistiche
Ottimizza i punteggi dei candidati della modalità rispetto a un valutatore. La rivalutazione indipendente verifica se lo stesso codice riceve lo stesso punteggio.
Le ipotesi preregistrate bloccano l'analisi prima delle esecuzioni di conferma. Il motore valuta le esecuzioni memorizzate utilizzando i test per campione singolo o i test di Welch supportati e effettua le regolazioni tra le preregistrazioni della missione con la correzione di Holm. Esecuzioni mancanti, fallite o in sospeso possono rendere un risultato inconcludente. Valori identici deterministici non contano come conferma statistica.
Prove formali
Il controllore compila Lean 4 con il Mathlib fissato e verifica il risultato in un processo separato e affidabile. Rifiuta lacune nella prova e assiomi o metaprogrammazione non supportati.
Una prova accettata non è sufficiente di per sé: un giudice delle affermazioni confronta il teorema e le sue definizioni locali con l'affermazione effettiva. Affermazioni più deboli, diverse o non verificate non conferiscono all'affermazione il livello formalmente dimostrato.
Revisione umana
Un ricercatore può invitare un esperto esterno al team di ricerca a revisionare un'affermazione tramite un link con token inviato via email. L'esperto può confermare, rifiutare o richiedere ulteriore lavoro. Il rifiuto di un esperto segna l'affermazione come confutata.