Jádro Leanu propustilo neplatný důkaz, že nula je jedna, a oprava vyšla týž den

Vezměte si přirozené číslo. Je-li sudé, vydělte ho dvěma; je-li liché, vynásobte třemi a přičtěte jedničku. Collatzova domněnka říká, že se z každého kladného čísla takhle po konečně mnoha krocích dostanete k jedničce. Dokázat to nikdo neumí a patří to mezi nejznámější otevřené problémy matematiky.

Repozitář CollatzLean, který se 25. července objevil na GitHubu, přesto tvrdil opak. Vznikl podle de Mourova zápisu s pomocí umělé inteligence. Samotné znění má v souboru Collatz/Definitions.lean, kde je Collatzův krok napsaný přesně tak, jak stojí výš, a závěr v Collatz/Main.lean zní not_conjecture : ¬ Conjecture, tedy domněnka neplatí. Projekt se přeložil systémem Lean 4 a neobsahoval ani jedno sorry, což je značka, kterou Lean zaznamená vynechané místo v důkazu.

Nebyl to důkaz. Byla to chyba v jádře Leanu.

Co jádro nekontrolovalo

Lean má práci rozdělenou na dvě části. Zápis, který píše člověk, zpracuje elaborátor, tedy velký a složitý kus programu, kterému se z principu nevěří. Výsledkem je důkazní term a ten teprve přebírá jádro, malý program, jehož jedinou úlohou je term znovu zkontrolovat. Když projde jádrem, důkaz platí. Celá důvěryhodnost systému tedy stojí na těch pár tisících řádcích jádra.

Kiran Gopinathan původní repozitář rozebral a 28. července z něj vydestiloval krátký příklad, který jádru předloží důkaz nepravdy. Podal ho jako hlášení #14576 s nadpisem, který přeložen říká, že jádro přijímá projekce s nesprávnou strukturou a dovoluje tím bezaxiomový důkaz nepravdy. Příklad nesahá na sorry, na unsafeCast, na vypnutou kontrolu ani na upravené soubory .olean.

Příčinu popsal Leonardo de Moura, hlavní architekt Leanu, ve vlastním zápisu z 1. srpna. Když jádro zpracovává vnořený výskyt pod induktivním typem, jehož parametry se v polích konstruktorů vůbec neobjeví, tyto parametry vypadnou z pomocného typu, který si jádro k té práci vyrábí. A co vypadne, to se nekontroluje. Špatně otypovaný výraz na tom místě pak stačil k tomu, aby jádro přijalo důkaz nepravdy, a z nepravdy plyne cokoliv, tedy i to, že nula se rovná jedné.

Dvě věci k tomu de Moura dodává. Zaprvé, chyba je dosažitelná jen metaprogramováním: deklarace se musí jádru poslat přímo, protože běžnou cestou ji elaborátor zachytí. Zadruhé je to podle něj chyba v implementaci, ne díra v metateorii Leanu.

Nezávislý kontrolor ho pustil taky

Obvyklá pojistka proti chybě v jádře je přepočítat důkaz jinou, nezávisle napsanou implementací. Pro Lean je jí nanoda, kterou v Rustu píše Chris Bailey. Collatzův repozitář prošel i jí, přesněji její týden starou verzí, a to je na celé věci nejzajímavější: nešlo o jednu chybu, ale o dvě, které spolu nesouvisejí. Oficiální jádro neprovádělo kontrolu u vnořených induktivních typů, kdežto nanoda tohle místo kontrolovala, zato neověřovala jméno struktury v uzlu projekce. Podle de Moury byl ten důkaz postavený tak, že výraz, kam se oficiální jádro nepodívá, byl přesně ten, který tehdejší nanoda propustila.

Chybu v nanodě nahlásil Jeremy Chen a opravená byla už týden předtím, než se objevilo hlášení proti Leanu. Ramana Kumar, autor repozitáře, považuje shodu okolností za náhodu, ale podle de Mourova zápisu nevylučuje, že model, se kterým důkaz vznikal, hlášení o nanodě viděl. Joachim Breitner nabídl jiné vysvětlení: shoda plyne z toho, že jsou dnes k dispozici modely, které takovou chybu najdou.

Praktický závěr z toho vychází mírnější, než se na první pohled zdá. Kontrola nezávislým jádrem dál funguje, protože k obejití bylo potřeba obejít dvě různé implementace naráz. Kdo se na ni spoléhá, potřebuje ale aktuální verze obou. Formalizace lean4lean od Maria Carneira, která má o Leanově typové teorii dokázat, že ji jádro implementuje správně, tou chybou zasažená je, protože její zpracování induktivních typů je převzaté z referenční implementace.

Od hlášení k opravenému vydání za den

Hlášení #14576 vzniklo 28. července v 3.28 UTC. Žádost o začlenění #14577 podal de Moura v 5.08 téhož dne a začleněná byla v 13.39. Je v ní 111 přidaných a 3 odebrané řádky ve třech souborech, přičemž vlastní oprava v src/kernel/inductive.cpp dělá 14 přidaných a 3 odebrané řádky; zbytek jsou dva testy, které přesně ten příklad z hlášení zkoušejí znovu. Jádro nově dotyčné argumenty zkontroluje na konci, až má k dispozici právě deklarované induktivní typy.

Opravené vydání v4.32.2 vyšlo týž den. Noční sestavení nightly-2026-07-29 odpovídá přímo tomu commitu s opravou.

Kde se oznámení a repozitář rozcházejí

Do konference oss-security poslal 2. srpna vlastní oznámení Jonathan Brossard. Přidal k němu ukázku v Dockeru, která na verzi 4.31.0 dokáže 0 = 1 bez jediného axiomu, ohodnocení CVSS 3.1 na 7,1 bodu a zařazení pod CWE-843 (záměna typů) a CWE-20. Číslo CVE zatím přiděleno není; Brossard k tomu píše, že projekt Lean nemá soubor SECURITY.md ani zapnuté neveřejné hlášení zranitelností na GitHubu.

Dvě věci v tom oznámení ale nesedí a rozhodne o nich sám repozitář. Zasažené jsou podle něj verze „do 4.31.0 včetně“, jenže Collatzův repozitář má Lean i Mathlib přišpendlené na 4.32.1 a prošel. A hlavně: oznámení tvrdí, že v době jeho vydání neexistuje opravené stabilní vydání. Přitom značka v4.32.2 je ze 28. července a soubor s testem tests/elab/issue_14576.lean v ní je, kdežto ve značce v4.32.1 chybí; totéž platí o samotné kontrole v src/kernel/inductive.cpp. Opravené stabilní vydání tedy bylo venku čtyři dny před tím oznámením.

Co po tom zůstalo

Návazná žádost #14582, která má jádro donutit ověřovat, že se parametry vnořeného výskytu opravdu chovají jako parametry, je zatím otevřená. Daniel Selsam z OpenAI pomohl nadaci Lean FRO modelem zaměřeným na bezpečnost a našel v jádře další chyby v programu; podle de Moury jsou všechny opravené, všechny byly dosažitelné jen metaprogramováním a všechny nanoda zachytila.

Zaznělo taky, že by se metaprogramování mělo omezit, aby se takový útok nedal vůbec zapsat. To de Moura odmítá: elaborátor je nedůvěryhodný záměrně a správnost nesmí stát na tom, že nějaká nedůvěryhodná součást odmítne sestavit špatný term. Kdo chce podstrčit vadný důkaz, může rovnou zapisovat soubory .olean nebo sáhnout do paměti. Jádro musí špatně otypované deklarace odmítnout samo.

Podle nás je na celém případu zajímavější než ta chyba to, co ukázala o pojistkách. Repozitář prošel jádrem i nezávislým kontrolorem, tedy oběma programy, které tohle mají odhalit, a přesto to nebyl důkaz. Poznal to až člověk, který ho rozebral na nejmenší kousek. Strojová kontrola důkazu je tak silná jako program, který ji provádí, a proti chybě v něm pomáhá jedině to, že ji někdo hledá.

Zdroje: zápis Leonarda de Moury z 1. srpna 2026, oznámení v konferenci oss-security z 2. srpna 2026, hlášení #14576 a oprava #14577 v repozitáři Leanu a repozitář CollatzLean. Data vydání a obsah značek v4.32.1 a v4.32.2 ověřeny přes rozhraní GitHubu.