🎀 Terence Tao spolupracuje s Math, Inc. 🎀 jako první Veritas Fellow — formalizovat odhady v teorii čísel. V analytické teorii čísel literatura obsahuje rozsáhlou síť explicitních odhadů. Ale tato síť není okamžitě interoperabilní. V praxi se výsledky projevují ve třech vrstvách: Primární odhady: Jedná se o základní vstupy, jako jsou oblasti bez nul pro Riemannovu zeta funkci. Často závisí na rozsáhlém výpočtu a pečlivé numerické optimalizaci. Sekundární odhady: Mnoho článků bere primární vstup (např. oblast bez nuly) a převádí jej na znovupoužitelné důsledky, například počítání prvočísel v krátkých intervalech. Tyto se stávají základními stavebními kameny používanými v celém předmětu. Terciární odhady: Další práce pak aplikuje tyto sekundární stavební bloky na frontierové číselné problémy, např. reprezentaci celých čísel jako součtu tří prvočísel. Problém je v tom, že tyto vrstvy se časem neaktualizují čistě. Vysokoškolský článek může spoléhat na nejlepší primární odhad v danou dobu. Ale o několik let později vylepšené výpočty zpřesňují primární vstup, aniž by byl systematicky propagován sekundárním a terciárním řetězcem. Výsledkem je, že "stejná věta s aktualizovanými konstantami" je často neznámá. Cílem je formalizovat klíčové články napříč těmito vrstvami a poté je abstrahovat tak, aby jejich závislosti byly explicitní, skládatelné a strojově kontrolovatelné. Dlouhodobou vizí je vytvořit živou síť důsledků: když se primární odhad zlepší, každý následný dopad je automaticky aktualizován. To promění matematickou literaturu v modulární software. Teorie čísel je silným testovacím případem, protože její odhady mají relativně jasnou strukturu a sdílenou sadu standardních vstupů a výstupů. Ale v mnoha oblastech, jako jsou parciální parciální diferenciální diferenciálnosti, výzkumníci neustále věnují úsilí úpravám: přizpůsobování lemat a hypotéz, překladu mezi neslučitelnými rámci, "zakládání čtvercových kolíků do kulatých děr." Na toto tření přímo cílí složatelná, strojem ověřená síť implikací. Stejná infrastruktura je připravena škálovat se i do jiných oblastí a umožnit crowdsourcingové, rozsáhlé projekty, které je v současnosti obtížné koordinovat. Klasickým příkladem je klasifikace konečných jednoduchých grup: desetiletí trvající úsilí rozdělené mezi mnoho přispěvatelů, s nevyhnutelnou složitostí kolem účetnictví, integrace a jistoty v úplnost. S moderními nástroji si představujeme řešení projektů srovnatelného rozsahu: mnoho přispěvatelů se zabývá různými případy a automatizované systémy slepují jednotlivé části dohromady. Pole se stává živým dashboardem pro průběh, který zaznamenává, co je ověřeno, co zůstalo a jaké závislosti každá komponenta vyžaduje. To otevírá možnost mnohem rychlejšího a zajímavějšího způsobu práce s matematikou. Podívejte se na Taoovu osnovu na YouTube: