Auslöser war eine mit KI-Hilfe erzeugte „Widerlegung“ der Collatz-Vermutung, die Ramana Kumar am 25. Juli veröffentlichte. Leans Prüfkern, der jeden Beweisschritt nachrechnet, nahm sie an, weil ihm bei verschachtelten induktiven Typen eine Prüfung fehlte. Der Fehler war am 28. Juli gemeldet und binnen einer Stunde behoben. Auch der unabhängige Prüfer nanoda ließ den Beweis durch, wegen eines zweiten, eine Woche zuvor behobenen Fehlers. Kumar hält das Zusammentreffen für Zufall, kann aber nicht ausschließen, dass das Modell die nanoda-Meldung kannte.
Daniel Selsam von OpenAI suchte danach mit internen Modellen gezielt weiter, bis das Modell am 20. August keine Lücke mehr fand. Über vier weitere Fehler brachte es den offiziellen Prüfkern dazu, einen Beweis des Widerspruchs „False“ anzunehmen, aus dem sich jede beliebige Aussage folgern ließe; einen davon ließ auch nanoda durch. Zwei Angriffe zielten auf die Laufzeitumgebung: ein überlaufender Referenzzähler, der Speicher beschädigte, und die veraltete Rechenbibliothek GMP 6.1.2 mit bekanntem Fehler in den Linux-Builds. Gruppen mit öffentlich verfügbaren Modellen meldeten laut de Moura keine Fehler.
Alle Fehler lagen in der Umsetzung, nicht in der Theorie hinter Lean, und waren nur über Metaprogrammierung erreichbar, also über Code, der Deklarationen direkt an den Prüfkern schickt. Ab Version 4.35.0 soll der Befehl lake check ein Projekt exportieren und mit einem zweiten Prüfer nachrechnen; weitere unabhängige Prüfkerne wie nanoda sollen mitgeliefert werden. Wer fremde oder KI-erzeugte Beweise abnimmt, soll laut de Moura nicht auf den normalen Build vertrauen, sondern das Werkzeug comparator und externe Prüfer nutzen.