prove

Skill do automatycznego tworzenia i weryfikacji formalnych dowodów matematycznych. Przeprowadza pięciofazowy proces: badanie dostępnych lematów w bibliotece Mathlib, projektowanie struktury dowodu, testowanie w Lean4, implementację oraz finalną weryfikację. Idealne dla matematyków, którzy chcą uzyskać maszynowo zweryfikowane dowody bez konieczności opanowania składni języka Lean. Obsługuje twierdzenia z teorii grup, topologii, algebry i innych dziedzin matematyki.

1. Sprawdź, czy Lean4 jest zainstalowany na Twoim systemie, uruchamiając polecenie lake --version. Jeśli Lean4 nie jest dostępny, zainstaluj menedżer wersji elan poprzez pobranie i uruchomienie skryptu inicjalizacyjnego z repozytorium leanprover/elan, następnie zrestartuj powłokę i potwierdź instalację poleceniem lake --version.
2. Przy pierwszym użyciu skill automatycznie pobierze bibliotekę Mathlib (około 2 GB) poprzez lake build — proces może potrwać kilka minut.
3. Wyzwól skill używając jednego z triggerów: /prove, /verify, /show that, /is it true lub /formalize, a następnie sformułuj twierdzenie, które chcesz udowodnić, na przykład /prove every group homomorphism preserves identity.
4. Skill przejdzie przez fazę badawczą, przeszukując bibliotekę Mathlib za pomocą narzędzia loogle w celu znalezienia odpowiednich lematów i strategii dowodu.
5. System automatycznie zaprojektuje strukturę dowodu, przetestuje ją w Lean4, zaimplementuje formalny kod i przeprowadzi weryfikację maszynową.
6. Otrzymasz w wyniku w pełni zweryfikowany dowód matematyczny, który możesz wykorzystać w swoich badaniach lub publikacjach.