loogle-search

Loogle Search to narzędzie dla matematyków i programistów pracujących z Lean, które pozwala wyszukiwać lematy w bibliotece Mathlib na podstawie wzorca sygnatury typu. Zamiast pamiętać dokładną nazwę funkcji, opisujesz kształt typu, który Ci potrzebny – na przykład szukając funkcji mapującej listy lub sprawdzając dostępne lematy dla grupy cyklicznej. Narzędzie obsługuje zmienne typów, symbole wieloznaczne i wyszukiwanie po nazwach. Z serwerem działającym w tle zapytania wykonują się w 100–200 ms, co sprawia, że praca nad dowodem staje się płynna i interaktywna.

1. Zainstaluj Loogle, budując projekt z katalogu ~/tools/loogle za pomocą polecenia lake build, a następnie lake build LoogleMathlibCache, aby wygenerować indeks Mathlib (zajmuje około 343 MB pamięci).

2. Uruchom serwer Loogle poleceniem loogle-server, aby przechowywać indeks w pamięci – dzięki temu kolejne zapytania będą szybsze (około 100–200 ms zamiast 10 sekund).

3. Gdy pracujesz nad dowodem w Lean i potrzebujesz lematu, ale znasz tylko kształt typu, użyj polecenia loogle-search z wzorcem. Na przykład loogle-search "Nontrivial _ ↔ _" znajdzie wszystkie lematy łączące Nontrivial z równoważnością, a loogle-search "(?a → ?b) → List ?a → List ?b" wyszuka funkcje mapujące listy.

4. W wzorcu używaj symbolu _ dla dowolnego typu, ?a i ?b dla zmiennych typów (ta sama zmienna oznacza ten sam typ), przecinków do wyszukiwania wielu pojęć naraz (np. "IsCyclic, center") oraz notacji Foo.bar dla dokładnego dopasowania nazwy.

5. Przejrzyj wyniki – Loogle zwraca listę pasujących lematów z ich sygnaturami. Jeśli chcesz wynik w formacie JSON, dodaj flagę --json do polecenia.

6. Skopiuj nazwę znalezionego lematu do swojego dowodu w Lean i kontynuuj pracę – na przykład exact Fintype.one_lt_card_iff_nontrivial, jeśli szukałeś lematu łączącego Nontrivial z kardynalnością.