M 348 Formalizace neformálně
DESCARTES, v.o.s. si vyhrazuje právo změnit termín konání akce, pokud bude nutné. O změně termínu se účastníci dozví s dostatečným časovým předstihem prostřednictvím pozvánky.
Obsah akce
Seznámíme se s jazkem Lean (https://lean-lang.org/), pomocí kterého budeme učit počítač automaticky kontrolovat matematické důkazy (a občas s nimi i přicházet). Budeme prakticky řešit zábavné problémy a prozkoumáme, jaké přínosy má tento směr pro pedagogiku, výzkum, i hlubší vhledy do matematiky. Jedná se o poměrně náročné téma, které nejspíš nepůjde v ZŠ a SŠ hodinách využít přímo, znalost jeho principu však výrazně prohlubuje formální myšlení, ke kterému pak lze vést i mladé žáky.
- motivace, filozofie a stručná historie počítačové formalizace matematických důkazů (1h)
- formální budování přirozených čísel a jejich vlastností v jazyce Lean (6h)
- vyhlídky do budoucna, zajímavé projekty, interakce s umělou inteligencí (1h)
Vzdělávací cíl
Porozumění významu formalizace a důkazových asistentů, budování formálního myšlení, získání základních dovedností v jazyce Lean.
Pro účastníky
Co si mají účastníci donést s sebou
Notebook s webovým prohlížečem a nabíječkou, papír a psací potřeby. V případě webináře: PC se softwarem ZOOM pro účast na webináři s mikrofonem pro případné dotazy. Webkamera je také vhodná, ale není nutnou podmínkou účasti.