Nieformalne wycieczki po dowodach

Dzisiaj Ryan Williams opublikował artykuł na temat arXiv (wcześniej ukazał się w SIGACT News) zawierający mniej techniczną wersję swojej najnowszej techniki ACC z dolną granicą.

Moje pytanie nie dotyczy samej techniki (oczywiście godnej wielkiej pochwały), ale dotyczy stylu pracy. W streszczeniu pisze:

Dowód zostanie opisany z perspektywy osoby próbującej go odkryć.

Niesamowite! W sekcji Tło dodaje:

Ten artykuł jest dyskusją o tym, jak odkryć dowód - swobodną wycieczkę po nim. Nie wszystkie szczegóły zostaną podane, ale zobaczysz, skąd pochodzą wszystkie elementy i jak się ze sobą łączą. Ścieżka będzie zaśmiecona moimi stronniczymi intuicjami na temat teorii złożoności - co moim zdaniem powinno i nie powinno być prawdą, i dlaczego. Wiele z tej intuicji może się mylić; jednak mogę powiedzieć, że przynajmniej raz przywiodło mnie ono w produktywnym kierunku.

To niesamowite i po raz pierwszy to widziałem. Zawsze zastanawiałem się, dlaczego autorzy papieru nie piszą, jak dostali się do dowodu, w tym nieudanego podejścia, które wypróbowali przed dotarciem na ścieżkę prowadzącą do rozwiązania. Kiedy zobaczyłem artykuł Ryana na arXiv, poczułem wielką motywację do jego przeczytania. Z tego punktu widzenia uważam to za rewolucyjny artykuł. Przez większość czasu jedyną rzeczą, którą możesz zrobić z papierem, jest sprawdzenie jego poprawności.

Pytanie jest następujące:

• czy zdajesz sobie sprawę z innych artykułów w TCS, w których przełomowy wynik jest przedstawiany w „swobodnej trasie”, a nie w serii technicznych lematów?

Mówię o publikacjach w czasopismach, a nie na blogach i raportach technicznych.

Ponadto oznaczyłem go jako dużą listę , mając nadzieję, że tak się stanie.

Istnieje artykuł (2001) o podobnym stylu autorstwa Lov Grovera, który opisuje drogę do jego przełomowego algorytmu wyszukiwania kwantowego (1996).

Tim Gowers jest fanem tego rodzaju rzeczy. Zobacz w szczególności jego objaśnienie metody przybliżenia Razborowa .

We wstępie Gowers powołuje się na mój artykuł w temacie wymuszania , który jest (nie do końca udaną) próbą zrobienia tego samego w celu wymuszenia. Wymuszanie jest zwykle uważane za technikę w logice i teorii mnogości, ale czasami trafia do TCS. Pojawia się w badaniu ograniczonej złożoności arytmetycznej i dowodowej zdania (Krajíček i Takeuti to dwaj badacze, którzy dążyli do tego związku), a pojęcie ogólnej wyroczni związane jest z koncepcją filtra ogólnego.

(Zaczęło się od komentarza i stało się zdecydowanie za długie).

Możesz cieszyć się artykułem Williama Thurstona O dowodzie i postępach w matematyce .

Matematyka w pewnym sensie ma wspólny język: język symboli, definicje techniczne, obliczenia i logikę. Ten język skutecznie przekazuje niektóre, ale nie wszystkie, tryby myślenia matematycznego. Matematycy uczą się tłumaczyć pewne rzeczy niemal nieświadomie z jednego trybu mentalnego na drugi, aby niektóre stwierdzenia szybko stały się jasne. [...]

Ludzie zaznajomieni ze sposobami robienia rzeczy na subpolu rozpoznają różne wzorce wypowiedzi lub formuł jako idiomy lub obrzezanie pewnych pojęć lub obrazów mentalnych. Ale dla ludzi, którzy nie są zaznajomieni z tym, co się dzieje, te same wzory nie są zbyt pouczające; często są nawet mylące. Język nie jest żywy, z wyjątkiem tych, którzy go używają. [...]

My, matematycy, musimy włożyć dużo więcej wysiłku w komunikowanie matematycznych pomysłów. Aby to osiągnąć, musimy poświęcić znacznie więcej uwagi komunikowaniu nie tylko naszych definicji, twierdzeń i dowodów, ale także naszych sposobów myślenia. Musimy docenić wartość różnych sposobów myślenia o tej samej strukturze matematycznej. Musimy skoncentrować znacznie więcej energii na zrozumieniu i wyjaśnieniu podstawowej infrastruktury mentalnej matematyki - w konsekwencji mniej energii na najnowsze wyniki. Wymaga to opracowania języka matematycznego, który jest skuteczny w radykalnym celu przekazywania pomysłów ludziom, którzy ich jeszcze nie znają.

Jeśli chodzi o oryginalne pytanie, istnieją artykuły, które nie przedstawiają pomysłów w formacie Definition-Theorem-Proof (DTP). Timothy Chow ma kilka artykułów, które koncentrują się na przekazywaniu pomysłów (choć nie są to pierwsze (lub drugie) artykuły na ten temat / wynik).

1. Mogłeś wymyślić sekwencje spektralne , Timothy Chow, Powiadomienia z AMS
2. Zmuszanie do manekinów , Timothy Chow

Jednym z możliwych powodów rozpowszechnienia formatu DTP jest to, że wszyscy jesteśmy przyzwyczajeni do tego z książek i dokumentów. Recenzenci (i czytelnicy) czasami zauważają, że niestandardowy styl pisania rozprasza uwagę. Środek stanowi papiery, które delikatnie psują czytelnika do wyniku. Istnieją prace przedstawiające szczególny przypadek lub prosty problem ilustrujący ogólną ideę.

1. Topologiczna struktura obliczeń asynchronicznych , Maurice Herlihy i Nir Shavit. Artykuł zawiera wiele ilustracji i pokazuje ogólną ideę prostego protokołu przed zastosowaniem głównego twierdzenia w celu rozwiązania niektórych otwartych problemów.
2. Logika i rozpoznawalny zestawy liczb$p$ , Véronique Bruyàre Georges Hansel, Christian Michaux i Roger Villemaire. Ekspozycja w stylu ankiety z pięknym rezultatem: zbiory liczb naturalnych, które są kodowane przez automaty skończone, niezależnie od wybranej bazy, są dokładnie tymi, które można zdefiniować w arytmetyki Presburger'a. Artykuł zawiera wiele przykładów, obejmuje przypadki szczególne przed sprawą ogólną i przedstawia tło historyczne dotyczące błędnych prób dowodowych.

Żadna dyskusja na temat niestandardowej prezentacji niezwykłych pomysłów nie byłaby kompletna bez wspomnienia o pracy Jean-Yvesa Girarda . Unikat jest prawdopodobnie najlepszym słowem, aby je opisać (nie będąc dyplomatycznym ani sarkastycznym). Z papierowej logiki liniowej .

Egzegeza filozoficzna reguł Heytinga pozostawia w rzeczywistości bardzo mało miejsca na dalszą dyskusję na temat rachunku intuicyjnego; ale czy ktoś kiedykolwiek poważnie próbował? W rzeczywistości logikę liniową, która jest wyraźnym i czystym rozszerzeniem zwykłej logiki, można osiągnąć poprzez bardziej dogłębną analizę semantyki dowodów (niezbyt daleko od podejścia informatycznego, a tym samym przeniesienia do następnej sekcji), lub przez pewne mniej lub bardziej bezpośrednie rozważania dotyczące rachunku różniczkowego. Te rozważania mają bezpośrednie znaczenie geometryczne, ale aby je zrozumieć, trzeba zapomnieć o intencjach, pamiętając z chińskim przywódcą, że nie liczy się kolor kota, ale fakt, że łapie on myszy.

Później:

Nadal są ludzie, którzy twierdzą, że aby stworzyć informatykę, potrzebna jest lutownica; tę opinię podzielają logicy, którzy gardzą informatyką, oraz inżynierowie, którzy gardzą teoretykami. Jednak w ostatnich latach potrzeba logicznego studium programowania stała się coraz wyraźniejsza, a połączenie logiki z informatyką wydaje się nieodwracalne. [...]
W pewnym sensie logika odgrywa tę samą rolę, co fizyka geometrii: rama geometryczna narzuca pewne wyniki konserwacji, na przykład formułę Stokesa. Symetrie logiki najprawdopodobniej wyrażają głęboką ochronę informacji w formie, która nie została jeszcze właściwie konceptualizowana.

Być może autorzy nie uwzględniają tych nieudanych prób i historii badań w swoich opublikowanych artykułach z powodu ograniczeń narzuconych przez redaktorów i członków komputerów. Wydaje mi się, że czasopismo (i prawdopodobnie jeszcze bardziej niezwykłe w przypadku konferencji) jest bardzo nietypowe, aby zaakceptować artykuł, w którym jego główna część jest poświęcona nieudanym próbom. Ale w większości przypadków, jeśli rozmawiasz z autorami lub ekspertami w tej dziedzinie, wyjaśnią historię i nieudane próby (i wielu mówi o tym na warsztatach).

Widziałem kilku autorów, którzy wyjaśniali podczas najmu, skąd pochodzą pomysły w ich artykułach. Jako przykład Girard wyjaśnia w swoim artykule, że pomysł na logikę liniową zrodził się z próby znalezienia denotacyjnej semantyki dla intuicyjnego OR. Tego rodzaju informacje można znaleźć również w monografiach i biografiach znanych badaczy oraz poświęconych im tomach ( autobiografia Halmosa i nowsze „Kreiseliana: About and Around Georg Kreisel ” pod redakcją Odifreddiego, są też tomy i artykuły poświęcony niektórym teoretykom złożoności). Mam nadzieję, że więcej osób zrobi to, co zrobił Ryan, i systematycznie wyjaśni proces i opowie historię.

ps: można to traktować jako ustną tradycję badań :) (nieco podobną do Tory Ustnej, której nie można było zapisać ).

Opublikowano artykuł Laszlo Babai (1990) w formie bajki o Arthurze i Merlinie opisujący dramatyczną sekwencję wydarzeń prowadzących społeczność do wyniku IP = PSPACE w 1989 r., Który był bardzo niewiarygodny zaledwie rok wcześniej.