Co je Lean?
Matematické důkazy mají výrazný rovnostářský rys – v zásadě si jejich platnost může ověřit úplně každý. Stačí sledovat řetězec nadčasových logických úvah, vycházejících z daných axiomů. Pokud jste však někdy zkusili ověřit všechny kroky v pokročilém matematickém důkazu, nejspíš víte, že v praxi je to obvykle vypadá úplně jinak — množství práce a nezbytných znalostí je obrovské. To je důvod, proč se mnoho matematiků a informatiků začalo zajímat o softwarové dokazovací asistenty a nástroje pro formální verifikaci (již v 60. letech!), jako je HOL, Coq, Agda, Isabelle a v neposlední řadě Lean – jež je předmětem tento série blogových příspěvků.
Proč tedy zvolit Lean oproti alternativám? Ostatně žádný „nejlepší přístup“ neexistuje – všechny tyto systémy využívají různé techniky a mohou se navzájem inspirovat. Ačkoli je Lean vhodný pro moderní matematiku, jeho hlavním lákadlem je pravděpodobně jeho velmi aktivní komunita, která překročila kritické množství. Jedním z největších počinů je působivá knihovna Mathlib, jejímž cílem je sjednotit co nejvíce matematiky kompatibilním a dostatečně obecným způsobem. To otevírá dveře mnoha matematikům, kteří by možná jinak neměli zájem. Existují také další zajímavé projekty, např. Liquid Tensor Experiment – úspěšná formalizace komplexního výsledku na okraji aktuálního poznání. Před pár lety to možná nebylo myslitelné a opravdu se zdá, že je tu nová éra matematiky. Přidáme-li do k tomu umělou inteligenci, můžeme být velmi brzy svědky zajímavého vývoje. Představte si, co bychom mohli dělat s veškerým intelektuálním kapitálem, který by už nebyl vázán kontrolou stovky stran technických důkazů!
Proč začít
Pokud vám nestačí stát se průkopníkem v potenciálně revoluční oblasti, tady jsou některé další pádné důvody:
- Je to dost zábavné, skoro jako videohra! Jak ukazuje výše uvedený snímek interaktivního infoview, můžete v každém okamžiku vidět aktuální hypotézy a cíle. Musíte jen najít správnou kombinaci příkazů k vyřešení hádanky, což může být velmi uspokojivé.
- Zbystřete své matematické myšlení tím, že jasně uvidíte strukturu svých důkazů. I když tématu dobře rozumíte, můžete získat nové poznatky (např. které části důkazu lze zobecnit do jiných kontextů, kolik informací nesou různé definice,…). Koneckonců učit něco je nejlepší způsob, jak něco plně pochopit, a mít jako studenta nemilosrdný a pečlivý jazyk je pro tento účel perfektní.
- Účast na zajímavých interdisciplinárních projektech, které by jinak nebyly dostupné. Např. i když nemáte požadovaný teoretický základ, stále můžete pracovat na softwarovém inženýrství a naopak.
- Nemůžete si vybrat mezi matematikou a programováním? Žádný strach, nyní můžete dělat obojí současně!
- Trénujte svou duševní odolnost tím, že vydržíte veškeré utrpení způsobené neúplnou dokumentací, nedostatkem tutoriálů a živými změnami jazyka. Vážně, toto může být nejslabší bod setkání s Leanem pro začátečníky, takže buďte připraveni čelit překážkám. (To je také hlavní důvod pro vznik této série, zaměřenou hlavně na psaní taktik.) Dobrá zpráva je, že port Mathlibu z Leanu 3 na Lean 4 byl nedávno dokončen, takže by se situace brzy měla zlepšit. Mezitím je Zulip tím nejlepším místem, kde se můžete ptát.
Jak začít
Chcete-li hrát s Leanem, dobrým vstupním bodem může být Natural number game; můžete také použít online Playground. Ale jakmile se rozhodnete pro serióznější použití, měli byste si pořídit lokální instalaci. Pro konkrétnější příklad použití můžete postupovat dle README našeho projektu (o něm více později).
Jestli jste stále tu, pojďme se ponořit hlouběji a něco fakt udělat v příštím příspěvku!
Pokud máte návrhy na zlepšení tohoto článku, dejte mi prosím vědět.