Robocikowo>ROBOCIKOWO
Wnioskowanie

Lean 4

2013AktywnyOpublikowano: 16 października 2026Aktualizacja: 16 października 2026Opublikowany
Otwartoźródłowy funkcyjny język programowania i interaktywny asystent dowodzenia twierdzeń oparty na teorii typów zależnych.
Kluczowa innowacja
Połączenie zależnego systemu typów (Calculus of Inductive Constructions) z wydajnym językiem programowania funkcyjnego, dzięki czemu dowody matematyczne i weryfikowalny kod powstają w jednym środowisku, a sam asystent dowodzenia jest w pełni rozszerzalny w samym Lean.
Kategoria
Wnioskowanie
Poziom abstrakcji
System
Poziom operacji
InferencjaŚrodowisko agentowe
Zastosowania
Formalizacja matematykiWeryfikacja oprogramowania i sprzętuAutomatyczne dowodzenie twierdzeń w AIInteraktywne dowodzenie twierdzeńNauczanie logiki i matematyki formalnejProgramowanie funkcyjne

Jak działa

Użytkownik zapisuje definicje i twierdzenia w języku z typami zależnymi, w którym twierdzenie jest typem, a jego dowód — termem tego typu (korespondencja Curry'ego-Howarda). Dowody buduje się interaktywnie za pomocą taktyk (np. simp, grind, induction), które przekształcają cel dowodowy aż do jego zamknięcia. Elaborator rozwija notację, wnioskuje typy i rozwiązuje instancje klas typów, a następnie minimalne, zaufane jądro ponownie sprawdza wygenerowany term dowodowy. Lean 4 kompiluje program do kodu C, a jego higieniczny system makr pozwala rozszerzać składnię i automatyzację bezpośrednio w samym Lean.

Rozwiązany problem

Nieformalne dowody matematyczne i zwykły kod mogą zawierać ukryte błędy, których nie wykrywa recenzja ani testy. Lean pozwala zapisać twierdzenie lub własność programu w sposób formalny i maszynowo zweryfikować, że dowód jest kompletny i poprawny, redukując zaufanie do niewielkiego, sprawdzonego jądra.

Komponenty

Trusted kernelMinimalne, zaufane jądro ponownie weryfikujące każdy term dowodowy; jedyny komponent, któremu trzeba ufać co do poprawności.
ElaboratorRozwija notację, wnioskuje typy, rozwiązuje instancje klas typów i przekształca kod źródłowy w pełne termy dla jądra.
Tactic frameworkEkspresyjny język taktyk (np. simp, grind, induction) do interaktywnego i zautomatyzowanego budowania dowodów.
Hygienic macro systemHigieniczny system makr pozwalający rozszerzać składnię i automatyzację bezpośrednio w Lean.

Oficjalna

Implementacja

Implementacje referencyjne
lean4
Lean, C++ · Lean FRO
Oficjalna
mathlib4
Lean · Lean community
Pułapki implementacyjne
Niekompatybilność Lean 4 z Lean 3Wysoka

Lean 4 nie jest kompatybilny wstecz z Lean 3; kod i dowody z Lean 3 wymagają portowania (projekt mathport).

Dowód jest tak wiarygodny jak jądroŚrednia

Weryfikacja zależy od poprawności jądra; w 2026 r. rzekomy dowód obalający hipotezę Collatza okazał się opierać na błędzie w Lean, który następnie naprawiono.

Ewolucja

Oryginalny paper · 2015 · CADE-25 2015 · Leonardo de Moura
The Lean Theorem Prover (System Description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2013
Powstanie Lean
Punkt przełomowy

Leonardo de Moura rozpoczyna projekt w Microsoft Research; wczesne wersje (Lean 1 i 2) były eksperymentalne.

2017
Lean 3

Pierwsza umiarkowanie stabilna wersja (20 stycznia 2017), zaimplementowana głównie w C++; wokół niej rozwinęła się biblioteka mathlib.

2021
Lean 4
Punkt przełomowy

Przepisanie asystenta zdolne generować kod C; higieniczny system makr i implementacja frontendu w samym Lean. Niekompatybilne wstecz z Lean 3.

2023
Powstanie Lean FRO

Utworzenie nienastawionej na zysk Lean Focused Research Organization w celu poprawy skalowalności i użyteczności języka.

2024
AlphaProof dowodzi w Lean
Punkt przełomowy

Google DeepMind tworzy AlphaProof, dowodzący twierdzeń matematycznych w Lean na poziomie srebrnego medalisty Międzynarodowej Olimpiady Matematycznej.

AI achieves silver-medal standard solving International Mathematical Olympiad problems (artykuł)
2025
DeepSeek-Prover-V2

DeepSeek przedstawia DeepSeek-Prover-V2, model do dowodzenia twierdzeń w Lean 4 zbudowany na DeepSeek-V3.

Wymagania sprzętowe

Podstawowe

Lean 4 kompiluje się do kodu C i działa wieloplatformowo (Linux, macOS, Windows) na procesorach x86-64 oraz AArch64; nie wymaga akceleratorów.