M 348 Formalizace neformálně 03.02.2026, 10:00–17:00

Pořádá Descartes v.o.s.

 
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)

Doplňující informace: