Lean fa ricontrollare le prove a verificatori diversi

Una dimostrazione controllata dal computer si fida comunque di un programma: quello che decide se è corretta. Dopo bug trovati anche con l’aiuto dell’AI, Lean aggiunge un modo piuttosto concreto per diffidare di se stesso.

La versione 4.35.0 permette di esportare le prove e ricontrollarle con kernel diversi. Uno, con-leche, è scritto in Lean e ha una prova di consistenza; con-ron ne traduce il controllo in Rust, con una verifica della corrispondenza tra i due.

Resta necessario fidarsi di compilatori e runtime. Il controllo incrociato riduce però il rischio che lo stesso errore attraversi implementazioni diverse: una prova deve convincere più arbitri, costruiti in modi differenti.