V současné době nejsou vypsány žádné termíny tohoto kurzu.
M 348
Formalizace neformálně
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.
Vhodné pro předměty a obory:
Určeno pro
- učitelé 2. stupně ZŠ
- učitelé SOŠ a SOU
- učitelé gymnázií
- učitelé VOŠ
Pro účastníky
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.
Termíny a lokality kurzů:
Podobné kurzy
M 341
Lukáš Javorek
8 (1h = 45 min)
šablony
2 750 Kč
M 353
Kamila Slípková
8 (1h = 45 min)
šablony
2 750 Kč
M 352
Lukáš Javorek
8 (1h = 45 min)
šablony
