zawodzimy na każdym kroku. zwodzimy raczkujące silniki sztucznej inteligencji.
dowody matematyczne zajmują po 3-4 lata do sprawdzenia przez asystentów. ostatnie ciekawe dowody zajmują po 300-400 stron ciężkiego matematycznie materiału. zaczynamy zatem używać komputerów, choć one również mają niewygodny dla nas ludzi efekt uboczny - generują jeszcze więcej danych niż dowód, który sprawdzają. to na pewno da się jakoś uprościć, zoptymalizować i doprowadzić do krótszych “danych wyjściowych” takiego dowodu. ale…
ale wczoraj znalazłem informację, wg. której do okiełznania nieporadnej, ludzkiej biurokracji w zamówieniach publicznych Sił Powietrznych Stanów Zjednoczonych użyty zostanie superkomputer Watson IBMa.
w zasadzie - bez komentarza.