Naukowcy stworzyli system, który łączy sztuczną inteligencję z formalnym dowodzielem Lean 4, aby tworzyć matematycznie weryfikowalne certyfikaty dla analizy patentów. Rozwiązanie wykorzystuje teorię typów zależnych - zaawansowaną metodę z matematyki konstruktywnej, która pozwala na precyzyjne definiowanie i sprawdzanie poprawności logicznych twierdzeń. To znaczące posunięcie w kierunku zwiększenia niezawodności procesów patentowych, gdzie błędy mogą kosztować miliony dolarów i lata sporu sądowego.
Dotychczas analiza patentów polegała głównie na pracy ekspertów, którzy przeszukują bazy danych i literaturę naukową, szukając precedensów i stwierdzając, czy nowość rzeczywiście jest nowoczesna. To czasochłonne zadanie pełne uproszczeń i potencjalnych pomyłek. Nowy hybrydowy system zmienia podejście - AI generuje wstępne analizy, ale każdy wniosek jest formalnie dowodzony w środowisku Lean 4, które gwarantuje matematyczną pewność wyników. Oznacza to, że zamiast polegać na opinii eksperta, uzyskujemy maszynowo weryfikowalny certyfikat, którego poprawność można niezależnie zweryfikować.
Praktyczne konsekwencje są istotne zarówno dla urzędów patentowych, jak i firm zdające się na własność intelektualną. System mógłby znacznie przyspieszić procedury patentowe, zmniejszyć liczbę błędnych pozytywnych wyników i dostarczyć obiektywnych dowodów w sporach o naruszenie praw. Podejście to stanowi przykład bardziej ogólnego trendu - zastosowania formalnych metod weryfikacji do domen, gdzie stawka jest wysoka i gdzie dotychczas brak było narzędzi do pełnej automatyzacji. Choć badanie jest na etapie demonstracyjnym, pokazuje potencjał połączenia nowoczesnego AI z klasycznymi metodami dowodzenia matematycznego.