Dowód wyrażony w języku formalnym asystenta (np. taktyki Lean) jest redukowany do sekwencji zastosowań aksjomatów i reguł wnioskowania. Małe, zaufane jądro (kernel) sprawdza każdy krok; jeśli którykolwiek jest niepoprawny, cały dowód jest odrzucany. W pętli z AI: model generuje/uzupełnia dowód, weryfikator zwraca sukces lub błąd, a wynik służy jako sygnał do poprawy lub jako nagroda w treningu. Poprawność opiera się na zaufaniu do (bardzo małego) jądra oraz aksjomatów.
Rozumowanie LLM bywa przekonujące, lecz błędne (halucynacje). Formalna weryfikacja daje obiektywne, maszynowe kryterium poprawności dowodu, dostarczając AI wiarygodnego sygnału prawdy.
Małe, zaufane jądro sprawdzające każdy krok dowodu.
Formalny zapis dowodu (np. taktyki Lean) redukowany do reguł.
Oficjalna
Zbiór zweryfikowanych definicji i twierdzeń (np. mathlib).
Oficjalna
Weryfikacja jest tak wiarygodna, jak jądro i przyjęte aksjomaty.
Złożone dowody mogą być kosztowne obliczeniowo do sprawdzenia.
Powstaje jeden z kluczowych asystentów dowodzenia.
Microsoft Research inicjuje Lean; później baza mathlib.
Weryfikacja w Lean jako sygnał prawdy dla rozumowania AI (poziom medalowy IMO).
