Zespół badaczy zaproponował system wyszukiwania dowodów wspierany komunikatami kompilatora, który inteligentnie steruje procesem dowodzenia twierdzeń w projektach Lean 4. Zamiast podejmować chaotyczne próby, metoda uczy się z błędów zwracanych przez kompilator i wybiera najbardziej obiecujące kierunki eksploracji, jednocześnie chroniąc częściowo poprawne dowody przed degradacją.
Systemem kierują dwa główne mechanizmy. Pierwszy to eksploracja poprzez równoczesne generowanie dowodów z dwóch różnych modeli oraz ponowne próbkowanie, gdy wyszukiwanie utknie w martwym punkcie. Drugi to eksploatacja, czyli rafinacja najlepszego dotychczasowego dowodu z wykorzystaniem porównywania dowodów opartego na informacjach od kompilatora. To podejście przypomina balans między szukaniem nowych możliwości a pogłębianiem tego, co już działa.
Badacze testowali metodę na siedmiu rzeczywistych projektach z zestawu miniCTX-v2. Wyniki pokazują, że przy tym samym budżecie (pass@32) nowa metoda uzyskuje średnią poprawę wskaźnika sukcesu o 12,8 punktu procentowego, jednocześnie zmniejszając liczbę zapytań do modelu jezykowego o 21,9 procent. To oznacza bardziej ekonomiczne wykorzystanie zasobów obliczeniowych bez spadku efektywności - kluczowe dla praktycznego wdrażania automatycznych systemów dowodzenia.