{"id":195211,"date":"2026-11-10T13:55:20","date_gmt":"2026-11-10T12:55:20","guid":{"rendered":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/"},"modified":"2026-11-10T13:55:20","modified_gmt":"2026-11-10T12:55:20","slug":"diku-bits-genai-agents-x-proof-assistants","status":"publish","type":"event","link":"https:\/\/uniavisen.dk\/en\/event\/diku-bits-genai-agents-x-proof-assistants\/","title":{"rendered":"DIKU Bits &#8211; GenAI Agents x Proof Assistants"},"content":{"rendered":"<p>Speaker: Dmitriy Traytel, Datalogisk Institut, Software, Data, People &amp; Society, Det Natur- og Biovidenskabelige Fakultet.<\/p>\n<p>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\u2019 research fields and create a common meeting space for both staff and students.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Speaker: Dmitriy Traytel, Datalogisk Institut, Software, Data, People &amp; 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 [&hellip;]<\/p>\n","protected":false},"author":0,"featured_media":195212,"template":"","class_list":["post-195211","event","type-event","status-publish","has-post-thumbnail","hentry","event_category-foredrag"],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v28.8 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>DIKU Bits - GenAI Agents x Proof Assistants<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"DIKU Bits - GenAI Agents x Proof Assistants\" \/>\n<meta property=\"og:description\" content=\"Speaker: Dmitriy Traytel, Datalogisk Institut, Software, Data, People &amp; 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 [&hellip;]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/\" \/>\n<meta property=\"og:site_name\" content=\"University Post\" \/>\n<meta property=\"article:publisher\" content=\"https:\/\/www.facebook.com\/uniavis\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:site\" content=\"@Uniavisen\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/uniavisen.dk\\\/event\\\/diku-bits-genai-agents-x-proof-assistants\\\/\",\"url\":\"https:\\\/\\\/uniavisen.dk\\\/event\\\/diku-bits-genai-agents-x-proof-assistants\\\/\",\"name\":\"DIKU Bits - GenAI Agents x Proof Assistants\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/uniavisen.dk\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/uniavisen.dk\\\/event\\\/diku-bits-genai-agents-x-proof-assistants\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/uniavisen.dk\\\/event\\\/diku-bits-genai-agents-x-proof-assistants\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/uniavisen.dk\\\/wp-content\\\/uploads\\\/2026\\\/11\\\/dikubitsdmitriytrayteludenqr.png\",\"datePublished\":\"2026-11-10T12:55:20+00:00\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/uniavisen.dk\\\/event\\\/diku-bits-genai-agents-x-proof-assistants\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/uniavisen.dk\\\/event\\\/diku-bits-genai-agents-x-proof-assistants\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/uniavisen.dk\\\/event\\\/diku-bits-genai-agents-x-proof-assistants\\\/#primaryimage\",\"url\":\"https:\\\/\\\/uniavisen.dk\\\/wp-content\\\/uploads\\\/2026\\\/11\\\/dikubitsdmitriytrayteludenqr.png\",\"contentUrl\":\"https:\\\/\\\/uniavisen.dk\\\/wp-content\\\/uploads\\\/2026\\\/11\\\/dikubitsdmitriytrayteludenqr.png\",\"width\":1920,\"height\":1080},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/uniavisen.dk\\\/event\\\/diku-bits-genai-agents-x-proof-assistants\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/uniavisen.dk\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Events\",\"item\":\"https:\\\/\\\/uniavisen.dk\\\/event\\\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"DIKU Bits &#8211; GenAI Agents x Proof Assistants\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/uniavisen.dk\\\/#website\",\"url\":\"https:\\\/\\\/uniavisen.dk\\\/\",\"name\":\"University Post\",\"description\":\"Independent of management\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/uniavisen.dk\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-US\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"DIKU Bits - GenAI Agents x Proof Assistants","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/","og_locale":"en_US","og_type":"article","og_title":"DIKU Bits - GenAI Agents x Proof Assistants","og_description":"Speaker: Dmitriy Traytel, Datalogisk Institut, Software, Data, People &amp; 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 [&hellip;]","og_url":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/","og_site_name":"University Post","article_publisher":"https:\/\/www.facebook.com\/uniavis","twitter_card":"summary_large_image","twitter_site":"@Uniavisen","schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/","url":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/","name":"DIKU Bits - GenAI Agents x Proof Assistants","isPartOf":{"@id":"https:\/\/uniavisen.dk\/#website"},"primaryImageOfPage":{"@id":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/#primaryimage"},"image":{"@id":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/#primaryimage"},"thumbnailUrl":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr.png","datePublished":"2026-11-10T12:55:20+00:00","breadcrumb":{"@id":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/#primaryimage","url":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr.png","contentUrl":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr.png","width":1920,"height":1080},{"@type":"BreadcrumbList","@id":"https:\/\/uniavisen.dk\/event\/diku-bits-genai-agents-x-proof-assistants\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/uniavisen.dk\/en\/"},{"@type":"ListItem","position":2,"name":"Events","item":"https:\/\/uniavisen.dk\/event\/"},{"@type":"ListItem","position":3,"name":"DIKU Bits &#8211; GenAI Agents x Proof Assistants"}]},{"@type":"WebSite","@id":"https:\/\/uniavisen.dk\/#website","url":"https:\/\/uniavisen.dk\/","name":"University Post","description":"Independent of management","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/uniavisen.dk\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-US"}]}},"advancedCustomFields":{"event_category":{"term_id":73,"name":"Foredrag","slug":"foredrag","term_group":0,"term_taxonomy_id":73,"taxonomy":"event_category","description":"","parent":0,"count":868,"filter":"raw"},"start":"2026-11-17 12:15:00","add_end_time":true,"end":"2026-11-17 13:00:00","location":"Lille UP1, DIKU, Universitetsparken 1, 2100 K\u00f8benhavn \u00d8 ","host_name":"VILU, Heads of Studies at DIKU, and Datalogisk Fagr\u00e5d","ticket_link":"","event_is_free":true,"event_poster":{"ID":195212,"id":195212,"title":"dikubitsdmitriytrayteludenqr.png","filename":"dikubitsdmitriytrayteludenqr.png","filesize":524075,"url":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr.png","link":"https:\/\/uniavisen.dk\/en\/event\/diku-bits-genai-agents-x-proof-assistants\/dikubitsdmitriytrayteludenqr-png\/","alt":"","author":"0","description":"","caption":"","name":"dikubitsdmitriytrayteludenqr-png","status":"inherit","uploaded_to":195211,"date":"2026-11-10 12:55:20","modified":"2026-11-10 12:55:23","menu_order":0,"mime_type":"image\/png","type":"image","subtype":"png","icon":"https:\/\/uniavisen.dk\/wp-includes\/images\/media\/default.png","width":1920,"height":1080,"sizes":{"thumbnail":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-150x150.png","thumbnail-width":150,"thumbnail-height":150,"medium":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-480x270.png","medium-width":480,"medium-height":270,"medium_large":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-768x432.png","medium_large-width":768,"medium_large-height":432,"large":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-1280x720.png","large-width":1280,"large-height":720,"1536x1536":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-1536x864.png","1536x1536-width":1536,"1536x1536-height":864,"2048x2048":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr.png","2048x2048-width":1920,"2048x2048-height":1080,"featured-soft":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-290x163.png","featured-soft-width":290,"featured-soft-height":163,"featured-hard":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-290x180.png","featured-hard-width":290,"featured-hard-height":180,"narrow":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-700x394.png","narrow-width":700,"narrow-height":394,"extended":"https:\/\/uniavisen.dk\/wp-content\/uploads\/2026\/11\/dikubitsdmitriytrayteludenqr-990x557.png","extended-width":990,"extended-height":557}},"short_description":"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\u2019s progress in AI\u2013prover collaboration, present his own AI experiments with the Isabelle proof assistant on financial mathematics, runtime monitors, and Isabelle\u2019s core algorithms itself, and weigh the benefits and risks of (over)relying on AI in formal proofs.","old_url":""},"_links":{"self":[{"href":"https:\/\/uniavisen.dk\/en\/wp-json\/wp\/v2\/events\/195211","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/uniavisen.dk\/en\/wp-json\/wp\/v2\/events"}],"about":[{"href":"https:\/\/uniavisen.dk\/en\/wp-json\/wp\/v2\/types\/event"}],"version-history":[{"count":0,"href":"https:\/\/uniavisen.dk\/en\/wp-json\/wp\/v2\/events\/195211\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/uniavisen.dk\/en\/wp-json\/wp\/v2\/media\/195212"}],"wp:attachment":[{"href":"https:\/\/uniavisen.dk\/en\/wp-json\/wp\/v2\/media?parent=195211"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}