PaperFormalizer to system agentywny oparty na Lean, który automatyzuje proces wyszukiwania i zamykania luk logicznych w pracach naukowych bezpośrednio z kodem źródłowym LaTeX. System przeprowadza każdy artykuł przez pipeline: najpierw transkrypcja do grafu zależności, następnie audyt każdego twierdzenia pod kątem zgodności z intencją autora, niejednoznaczności i poprawności, a na koniec formalizacja i dowód każdego stwierdzenia w Lean wspartego Mathlib.
Klucz do podejścia PaperFormalizer stanowi bezpośrednia współpraca z autorem. Tylko twórca pracy wie dokładnie, co konkretne stwierdzenie powinno oznaczać i jak najlepiej naprawić lukę formalną w wyniku. Zawsze gdy pojawi się dwuznaczność, system zatrzymuje się i pyta autora, prezentując każdą naprawę zarówno w naturalnym języku, jak i symboli TeX. Autor podejmuje wszystkie decyzje, które mogą zmienić znaczenie tego, co twierdzi jego praca - system nigdy nie zmienia automatycznie głównych roszczeń badacze bez eksplicytnej zgody.
Wyjściem jest anotowana i zrewidowana wersja artykułu, raport ze zmianami i kod Lean, gdzie każda deklaracja linkuje się do odpowiadającego jej stwierdzenia. Toolkit autora rośnie wraz z każdą sformalizowaną pracą, a badacze mogą dzielić się swoimi zweryfikowanymi paperami - inni naukowcy bazujący na tej pracy mogą wtedy ponownie użyć jej kodu Lean. To oznacza potencjalnie przełomową zmianę w jak prowadzimy badania, bo trudność produkcji formalnie zweryfikowanych prac zawsze stanowiła barierę dla szerszego przyjęcia formalnej weryfikacji w nauce.