Universitetsavisen
Nørregade 10
1165 København K
Tlf: 21 17 95 65 (man-fre kl. 9-15)
E-mail: uni-avis@adm.ku.dk
Københavns Universitet
Uafhængig af ledelsen
Foredrag
Foredrag — Proof assistants mechanically check every step of a mathematical proof, but their steep learning curve keeps expert users scarce. Generative AI agents promise to ease this bottleneck: interacting via the Model Context Protocol (MCP), they draft, refine and repair proofs until the proof assistant accepts them. In this talk, Dmitriy will survey this year’s progress in AI–prover collaboration, present his own AI experiments with the Isabelle proof assistant on financial mathematics, runtime monitors, and Isabelle’s core algorithms itself, and weigh the benefits and risks of (over)relying on AI in formal proofs.
Date & Time:
Place:
Lille UP1, DIKU, Universitetsparken 1, 2100 København Ø
Hosted by:
VILU, Heads of Studies at DIKU, and Datalogisk Fagråd
Cost:
Free
Speaker: Dmitriy Traytel, Datalogisk Institut, Software, Data, People & Society, Det Natur- og Biovidenskabelige Fakultet.
DIKU Bits is a lecture series for students (and (Ph.D.) employees) about current research at DIKU, held every other week . The lectures aim to inspire choices of elective courses, project writing, etc., but also to provide greater insight into colleagues’ research fields and create a common meeting space for both staff and students.