Naukowcy stworzyli AutoIP, bibliotekę Lean w której klasyczna teoria regularyzacji liniowej wraz z podstawami analizy funkcjonalnej została sformalizowana przez agentów AI. Proof assistanty takie jak Lean weryfikują dowody matematyczne aż do aksjomatów, a ostatnie osiągnięcia w sztucznej inteligencji uczynią pisanie takich dowodów tańszym i szybszym. Formalne dowody mogą jedynie potwierdzać sformułowania, które dowodzą, więc zadanie człowieka sprowadza się do weryfikacji, czy każde formalne stwierdzenie rzeczywiście wyraża to, co było zamierzone.
Organizacja biblioteki wokół tego zadania pozwala recenzentom porównać formalne sformułowania z ich naturalnojęzykowych odpowiednikami bez konieczności czytania samych dowodów. Doświadczenie zespołu wskazuje, że główne zagrożenia tkwią w sformułowaniach twierdzeń, a nie w dowodach - a proste testy automatyczne mogą ujawnić błędy nawet w utartej literaturze naukowej. Projekt zdemonstruje to na przykładzie twierdzenia z podręcznika, którego hipoteza okazała się bardziej restrykcyjna niż pierwotnie stwierdzano.
AutoIP stanowi zaproszenie dla społeczności badaczy zajmujących się problemami odwrotnymi do rozszerzenia i budowania na tej bibliotece. Projekt pokazuje, jak AI może wspomóc matematykę poprzez tanią i skalowalne formalizację, a jednocześnie ujawnia istotne różnice między pewnością obliczeniową a intencją matematyczną - co może prowadzić do głębokich zmian w sposobie, w jaki matematycy publikują i weryfikują wyniki.