Formální obrat v matematice: Od lidské intuice ke strojové verifikaci – umělá inteligence a matematické důkazy

Přednášku s názvem Formální obrat v matematice: Od lidské intuice ke strojové verifikaci – umělá inteligence a matematické důkazy připravil a veřejnosti přednese doc. Mgr. Dušan Bednařík, Ph.D. z katedry matematiky Přírodovědecké fakulty Univerzity Hradec Králové při příležitosti volební členské schůze pobočky JČMF Hradec Králové. Po cca 60minutové přednášce bude následovat krátká přestávka a po ní volební členská schůze pobočky JČMF Hradec Králové.

Anotace
V posledních letech vznikají softwarové nástroje zvané proof assistants, které dokážou strojově ověřit správnost matematických důkazů. Přednáška přiblíží jeden z nich – Lean 4 a jeho rostoucí knihovnu formálně verifikovaných teorémů Mathlib. Na konkrétních příkladech uvidíme, jak formální verifikace mění spolupráci matematiků a jak se do tohoto procesu zapojuje umělá inteligence. Závěrem se pokusíme naznačit, co to znamená pro výuku i výzkum matematiky.