Zespół badaczy formalizował w asystencie dowodów Lean 4 matematyczny wynik dotyczący równania Vlasova, wykorzystując AI jako narzędzie wykonawcze pod kierunkiem matematyka. Dokument LaTeX zamieniany był na kod Lean etapami, gdzie matematyk pełnił rolę kierownika - określał definicje, kierował dekompozycją problemu i wskazywał luki w bibliotekach, a system AI pisał dowody. Gra wygrywana była, gdy kod kompilował się bezbłędnie, nie zawierał konstrukcji sorry i niezweryfikowanych założeń, a dowody opierały się wyłącznie na fundamentalnych aksjomatach Lean.
Formalizacja objęła pełny, aksjomat-czysty dowód dobrze postawienia problemu dla nieliniowego równania Vlasova za pośrednictwem trasy mean-field Dobrushin'a. Obejmowała istnienie i jednoznaczność rozwiązań, estymaty stabilności, limit mean-field oraz zasadę superpozycji dla okien czasowych. Podczas procesu wyłoniła się samowystarczalna warstwa matematyki transportu optymalnego - właściwości metryki Wasserstein-1 i twierdzenie dualności Kantorowicza-Rubinstein'a - stanowiąca około jedną szóstą całej formalizacji. Ta część mogła być od razu zintegrowana z biblioteką Mathlib.
Podejście to demonstruje nowy model współpracy między matematykami i systemami AI przy formalizacji złożonych wyników. Zamiast asystować pisaniu pojedynczych linii kodu, AI przejmuje wykonawstwo, podczas gdy matematyk zachowuje kontrolę strategiczną nad kierunkiem pracy. Stanowi to potencjalnie znaczący krok w kierunku masowej formalizacji matematyki i automatyzacji weryfikacji wyników naukowych.