
<?xml version="1.0" encoding="UTF-8"?>
<tiskova_zprava>
    <titulek>
        PŘEDNÁŠKA | Formální obrat v matematice: Od lidské intuice ke strojové verifikaci – umělá inteligence a matematické důkazy
    </titulek>
    <datum>
        19.3.2026
    </datum>
    <autor>
          | Univerzita Hradec Králové
    </autor>
    <perex>
        Datum konání: 23. 3. 2026 16:30
    </perex>
    <text>
        
Zveme vás na 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řednáší: doc. Mgr. Dušan Bednařík, Ph.D. z Katedry matematiky PřF UHK

Kdy: 23. 3. 2026 od 16:30

Kde: učebna S2 (přízemí)

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.

https://www.uhk.cz/cs/prirodovedecka-fakulta/prf/aktualne/prednaska-formalni-obrat-v-matematice-od-lidske-intuice-ke-strojove-verifikaci-umela-inteligence-a-matematicke-dukazy


    </text>
</tiskova_zprava>
