Lean dla programistów: co dowód formalny sprawdza, a czego nie zastąpi

Czym jest Lean i do czego służy programiście?

Lean jest jednocześnie językiem programowania i interaktywnym asystentem dowodów opartym na teorii typów zależnych. Dokumentacja opisuje go jako narzędzie przeznaczone zarówno do matematyki, jak i do weryfikacji oprogramowania. Kod i dowody zapisuje się w tych samych plikach, a o poprawności rozstrzyga kernel [1]. Programista przenosi więc część pracy z trybu „uruchom i sprawdź” na „zapisz, co ma być prawdą, i udowodnij to”. W AI do programowania taki dowód bywa warstwą kontroli nad kodem, który powstał szybciej, niż zdążono go przemyśleć.

Jak Lean wykrywa błędy, których nie widzą testy?

Dowód nie jest szybszym testem. Test uruchamia implementację na wybranych danych i porównuje wynik z oczekiwaniem. Lean sprawdza term dowodowy dla twierdzenia, które dotyczy wszystkich wartości spełniających założenia [1]. Dzięki temu klasa błędów związana z pominiętym przypadkiem granicznym przestaje zależeć od doboru testów. Granica jest jednak ostra: Lean rozstrzyga wyłącznie to, co zostało zapisane formalnie, i nie ocenia, czy zapis oddaje intencję autora. W AI do programowania to rozróżnienie jest podstawą sensownego użycia Lean, bo samo narzędzie nie wie, jaką własność powinien mieć program.

Jakie właściwości trzeba zapisać, żeby dowód sortowania miał sens?

Twierdzenie „funkcja zwraca listę” jest prawdziwe i bezużyteczne. Dla sortowania formalizuje się co najmniej dwie własności wyniku: uporządkowanie oraz bycie permutacją elementów wejściowych [5]. Ten zestaw wyklucza implementację, która gubi duplikaty albo zwraca dane wejściowe w niezmienionej kolejności. Właśnie dlatego dowód bywa skuteczny tam, gdzie testy przechodzą, a błąd siedzi w założeniu, którego nikt nie zapisał jako przypadku testowego.

Dowód formalny a testy jednostkowe — co sprawdza każde z nich?

Kernel sprawdza końcowy term dowodowy, a nie drogę, którą autor do niego doszedł. Błąd w taktyce nie podważa dowodu, jeśli kernel odrzuci niepoprawny term [1]. To upraszcza przegląd: recenzent czyta twierdzenie i założenia, a nie każdą linię skryptu dowodowego. Dokumentacja Lean wprost ostrzega jednak, że dowód nie zastępuje testów, bo testy badają wydajność, integrację, dane rzeczywiste i zachowanie poza modelem [2].

Jak sprawdzić, czy dowód jest kompletny i godny zaufania?

Lean ostrzega przy sorry, czyli miejscu, w którym dowód pominięto. Polecenie sprawdzania aksjomatów pozwala wykryć niekompletne dowody oraz dodatkowe założenia, na których opiera się twierdzenie [6][2]. Poza projektem działają kontrole niezależne: lean4checker odtwarza dowód przez kernel, a narzędzie comparator może korzystać z sandboxa i zewnętrznych checkerów [2]. Żadne z nich nie usuwa wszystkich założeń zaufania. Przenoszą je w inne miejsce i pozwalają je nazwać, co jest różnicą istotną przy audycie kodu.

Czy Lean jest wolny od błędów?

Nie. Projekt Lean4Lean opisuje niezależny checker napisany w Lean, a jego autorzy wskazują, że praca nad weryfikacją wykryła błąd soundness i doprowadziła do jego naprawy [3]. Terry Tao opublikował 9 października 2026 r. tekst o niezawodności Lean i roli AI w dowodzeniu [4]. Wniosek dla zespołu jest praktyczny: zaufanie do dowodu opiera się na zaufaniu do kernela i do sformułowanych twierdzeń, a nie na założeniu, że narzędzie jest bezbłędne.

Od czego zacząć z Lean 4?

Start polega na wybraniu konkretnej wersji i utrzymaniu jej w repozytorium razem z mathlib oraz konfiguracją budowania. Wydania zmieniają się szybko: 4.34.1 ukazało się 24 września 2026 r., a 4.35.0 — 12 października 2026 r. [7]. Dwa podstawowe teksty to dokumentacja referencyjna języka oraz podręcznik „Theorem Proving in Lean 4” [1][6]. Pierwszy dowód warto napisać o własności, której zespół naprawdę potrzebuje, a nie o przykładzie z tutoriala. W repozytorium przydają się też konwencje pracy opisane w artykule o plikach AGENTS.md, bo dowody są kodem, który ktoś będzie recenzował.

Czy dowód formalny pomaga przy kodzie generowanym przez AI?

Pomaga w wąskim zakresie. Model potrafi napisać implementację szybciej niż człowiek, ale nie odpowiada za to, czy spełnia własność, której nikt nie zapisał. Twierdzenie w Lean jest taką własnością w formie, którą da się sprawdzić maszynowo [1]. Tao opisuje jednocześnie szanse i ryzyka związane z użyciem AI w dowodzeniu, w tym kwestię zaufania do wyniku [4]. Praktyczny wniosek: dowód ma sens dla krytycznego fragmentu, a nie jako domyślna bramka dla całego repozytorium. Szerzej o łączeniu modeli z pracą zespołu piszę w materiale o integracji AI z kodem i dokumentacją.

Kiedy formalna weryfikacja ma sens w zespole?

Trzy warunki: własność da się zapisać formalnie, specyfikacja jest stabilna, a zespół ma czas na naukę składni i bibliotek. Typowe zastosowania to algorytmy, struktury danych i kod kryptograficzny. W zwykłej aplikacji webowej koszt bywa wyższy niż zysk, bo większość ryzyka leży w integracji i danych, których dowód nie obejmuje [2]. Przy projektach, gdzie model generuje większość implementacji, warto rozważyć dowód dla jednego, dobrze wybranego modułu. Decyzję ułatwia tabela z sekcji o testach: pokazuje, czego dowód nie sprawdzi.

Najczęstsze pytania

Czy Lean zastępuje testy jednostkowe?

Nie. Dowód obejmuje tylko własności zapisane formalnie, a dokumentacja wprost mówi, że testy badają wydajność, integrację i dane rzeczywiste, których model formalny nie opisuje [2]. W praktyce oba narzędzia odpowiadają na różne pytania: test na „czy to działa na tym wejściu”, dowód na „czy to jest prawdą dla wszystkich wejść z założeń”.

Jakie błędy wykrywa dowód w Lean?

Wykrywa naruszenia własności zapisanych w twierdzeniu, na przykład to, że wynik sortowania nie jest permutacją wejścia [5]. Nie wykrywa błędów w samym twierdzeniu, błędów poza zweryfikowanym kodem ani problemów wydajnościowych. To zawężenie jest cechą metody, nie wadą implementacji.

Czy Lean nadaje się do zwykłego kodu biznesowego?

Rzadko jako domyślne narzędzie. Kod biznesowy zmienia się szybciej niż twierdzenia, a większość usterek siedzi w integracjach i danych. Dowód sprawdza się w wyodrębnionym module, którego poprawność jest krytyczna i whose specyfikacja jest stabilna [2].

Jakiej wersji Lean używać?

Tej, którą zespół zapisał w repozytorium razem z mathlib i konfiguracją budowania. Wersje zmieniają się często: 4.34.1 wydano 24 września 2026 r., a 4.35.0 — 12 października 2026 r. [7]. Podanie wersji w artykule lub dokumentacji projektu jest warunkiem powtarzalności dowodu.

Czy warto sprawdzać dowód niezależnie?

Tak, jeśli wynik ma znaczenie poza zespołem. lean4checker odtwarza dowód przez kernel, a comparator może korzystać z sandboxa i zewnętrznych checkerów [2]. Nie usuwa to wszystkich założeń zaufania, ale pokazuje, na czym dokładnie opiera się twierdzenie o poprawności.

Źródła

1. The Lean Language Reference (Lean FRO, 2026)
2. Validating a Lean Proof (Lean FRO, 2026)
3. Lean4Lean: Verifying a Typechecker for Lean, in Lean — Mario Carneiro (arXiv, 2024)
4. What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI (Terry Tao, 2026)
5. The Lean Programming Language and Theorem Prover (ETAPS, 2026)
6. Theorem Proving in Lean 4 (Lean FRO, 2026)
7. Release Notes (Lean FRO, 2026)