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)

Vhodné pro předměty a obory:

Určeno pro

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.