ověřování důkazů

Společnost Axiom Math pomocí systému AxiomProver automaticky formálně ověřila důkaz takzvané věty 246. Ta říká, že existuje nekonečně mnoho dvojic prvočísel, jejichž rozdíl je 246, což je dosud nejmenší prokázaná pevná mezera tohoto typu; domněnka o dvojčatech s rozdílem dvě zůstává nevyřešena. Tým při práci vytvořil znovupoužitelnou knihovnu výsledků o mezerách mezi prvočísly, nešlo tedy jen o jednorázové zpracování jednoho důkazu. Formální ověření sice není absolutní zárukou bez chyb, představuje však velmi silnou kontrolu strojově čitelného důkazu. Autoři vidí širší využití podobných metod při prověřování správnosti a bezpečnosti kódu vytvářeného umělou inteligencí.