Verificări publice ale soluțiilor Lean

Casa rulează un judecător cu trei nuclee pe o soluție: comparatorul Lean FRO verifică că fiecare teoremă are exact enunțul fixat de provocare și folosește doar axiomele permise, apoi nucleul oficial Lean, nanoda și con-leche (un verificator demonstrat să nu accepte o dovadă pentru „fals”) o reverifică. Înscriem aici verdictul, semnat. Certificăm acceptarea de către nucleele numite, nu adevărul absolut și nici că enunțul formal redă intenția celui care l-a scris.

Vrei să-ți păstrezi soluția sigilată? Nu o trimite aici: dovedește-o local cu programul ZK și postează doar chitanța, ca certificat ZK. Chitanța se verifică matematic; demonstrația ta nu îți părăsește mașina. Certificate

Nicio verificare încă.