Leanstral 1.5 dowodzi twierdzeń matematycznych i przy okazji znajduje błędy w prawdziwym kodzie

Dowód w Lean 4 nie wybacza. Każdy krok musi przejść przez kontroler, który nie przepuszcza niczego niejasnego, więc ktoś, kto formalnie sprawdza twierdzenie matematyczne albo poprawność fragmentu kodu, potrafi stracić godziny na przekładanie jednej intuicji na sztywną składnię, dopisywanie brakujących lematów i gonienie za błędami kompilatora. To właśnie ta mozolność sprawia, że formalna weryfikacja, choć daje twardą gwarancję poprawności, wciąż pozostaje niszą.

Dla programisty, który na co dzień nie zajmuje się matematyką, brzmi to abstrakcyjnie, ale stawka jest bardzo konkretna. Zwykłe testy sprawdzają kod na tych przypadkach, które akurat przyszły ci do głowy, i milczą o całej reszcie. Formalny dowód idzie dalej, bo pokazuje, że funkcja spełnia swoją specyfikację dla wszystkich możliwych wejść, raz a dobrze. Tym samym językiem opisuje się i twierdzenia z matematyki, i własności prawdziwego kodu, choćby fragmentów napisanych w Rust.

Leanstral 1.5, wypuszczony 6 lipca przez Mistrala, uderzył prosto w tę mozolność. To darmowy model, który zachowuje się jak agent programistyczny, tylko że jego robotą nie jest zwykły kod, lecz dowody. Proponuje kod w Lean, uruchamia kontroler, czyta jego uwagi i poprawia próbę tak długo, aż dowód przejdzie albo wyczerpie się budżet. Po drodze może edytować pliki, odpalać polecenia w powłoce i korzystać z serwera języka Lean, usługi, która na bieżąco zwraca informacje o tym, co w kodzie się nie zgadza.