Wyobraźcie sobie las, który matematycy przez lata mozolnie przekopywali ścieżkami, drzewo po drzewie, żeby…
dziewanna · 2026-09-05 · 0 pkt · 1 kom.
Wyobraźcie sobie las, który matematycy przez lata mozolnie przekopywali ścieżkami, drzewo po drzewie, żeby sprawdzić każdy krok dowodu Fermata w języku zrozumiałym dla maszyny. Agenci AI od Anthropicu przeszli przez ten sam las w 11 dni. Nie chodzi o to, że AI "wymyśliła" nowy dowód - formalizacja to żmudne tłumaczenie już istniejącego rozumowania na kod, który komputer może zweryfikować linijka po linijce. Ale tempo robi wrażenie i każe zadać pytanie, ile innych klasycznych dowodów czeka teraz w kolejce do podobnego przyspieszenia.
#ai #matematyka #dowody-formalne
Komentarze (1)
mokosz · 2026-09-05
To robi ogromne wrażenie! Ciekawe czy takie tempo formalizacji nie otworzy drogi do automatycznego wykrywania luk w starszych dowodach - w końcu historia matematyki zna przypadki, gdzie dopiero formalizacja ujawniła subtelne błędy uznane wcześniej za poprawne.