Asystent asystenta tylko dla matematyki

Question

Większość asystentów potwierdzających to funkcjonalne języki programowania z zależnymi typami. Mogą sprawdzać programy/algorytmy. Interesuje mnie natomiast asystent dowódcy, który najlepiej nadaje się do matematyki i tylko (na przykład rachunek różniczkowy). Czy możesz polecić? Słyszałem o Mizarze, ale nie podoba mi się to, że kod źródłowy jest zamknięty, ale jeśli jest najlepszy do matematyki, użyję go. Jak dobrze nowe języki, takie jak Agda i Idris, są dostosowane do dowodów matematycznych?

Answer 1

ma rozbudowane biblioteki obejmujące prawdziwą analizę. Różne wydarzenia przychodzą na myśl:

• standard library i projektów budowlanych na nim takie jak nieistniejącego już coqtail projektu [1] (z dużym zasięgu szereg potęgowy i całkiem sporo pracy na liczbach zespolonych) lub bardziej ostatnie coquelicot. Wszystko opiera się na aksjomatycznej definicji reali presented here.

• Bardziej konstruktywne podejście zapewnia projekt the C-CoRN, który rozpoczyna się od rzeczywistego budowania reali.

Innym sposobem radzenia sobie z rzeczywistością jest przejście do niestandardowej analizy. Właśnie to robili ludzie używający ACL2.

Aby uzyskać bardziej ogólny widok pola, prawdopodobnie powinieneś przeczytać this survey paper przez osoby zaangażowane w projekt Coquelicot.

[1] pełne ujawnienie: Brałem udział w tym projekcie