{"id":1,"date":"2024-07-08T14:45:42","date_gmt":"2024-07-08T14:45:42","guid":{"rendered":"https:\/\/sites.exeter.ac.uk\/mathsblog\/?p=1"},"modified":"2024-07-08T16:01:21","modified_gmt":"2024-07-08T16:01:21","slug":"hello-world","status":"publish","type":"post","link":"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/","title":{"rendered":"Workshop: Interactive Theorem Proving in Education and Research"},"content":{"rendered":"<p>There will be a one-day workshop on 24 July 2024 and online, focused on how interactive theorem provers, like Lean and Isabelle, can be used in mathematics and computer science. This event is ideal for educators and researchers who use deductive proof.<\/p>\n<p>No prior experience is necessary: the day starts and ends with hands-on sessions that provide practical experience for those unfamiliar with Lean.<\/p>\n<p>To register and for more details see:<\/p>\n<p><a href=\"_wp_link_placeholder\" data-wplink-edit=\"true\">https:\/\/exlean.org\/workshop-interactive-theorem-proving-in-education-and-research-july-2024\/#<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>There will be a one-day workshop on 24 July 2024 and online, focused on how interactive theorem provers, like Lean and Isabelle, can be used in mathematics and computer science. This event is ideal for educators and researchers who use deductive proof. No prior experience is necessary: the day starts and ends with hands-on sessions [&hellip;]<\/p>\n","protected":false},"author":3,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[1],"tags":[],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v23.0 - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>Workshop: Interactive Theorem Proving in Education and Research - Department of Maths and Stats local<\/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:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Workshop: Interactive Theorem Proving in Education and Research - Department of Maths and Stats local\" \/>\n<meta property=\"og:description\" content=\"There will be a one-day workshop on 24 July 2024 and online, focused on how interactive theorem provers, like Lean and Isabelle, can be used in mathematics and computer science. This event is ideal for educators and researchers who use deductive proof. No prior experience is necessary: the day starts and ends with hands-on sessions [&hellip;]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/\" \/>\n<meta property=\"og:site_name\" content=\"Department of Maths and Stats local\" \/>\n<meta property=\"article:published_time\" content=\"2024-07-08T14:45:42+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2024-07-08T16:01:21+00:00\" \/>\n<meta name=\"author\" content=\"Jane Tanner\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"Jane Tanner\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/\",\"url\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/\",\"name\":\"Workshop: Interactive Theorem Proving in Education and Research - Department of Maths and Stats local\",\"isPartOf\":{\"@id\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/#website\"},\"datePublished\":\"2024-07-08T14:45:42+00:00\",\"dateModified\":\"2024-07-08T16:01:21+00:00\",\"author\":{\"@id\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/#\/schema\/person\/80ca16af2fbb5ea0718a2151f6973b7b\"},\"breadcrumb\":{\"@id\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Workshop: Interactive Theorem Proving in Education and Research\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/#website\",\"url\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/\",\"name\":\"Department of Maths and Stats local\",\"description\":\"\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"en-US\"},{\"@type\":\"Person\",\"@id\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/#\/schema\/person\/80ca16af2fbb5ea0718a2151f6973b7b\",\"name\":\"Jane Tanner\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/#\/schema\/person\/image\/\",\"url\":\"https:\/\/secure.gravatar.com\/avatar\/bb5b91fbdf9d62ff41ec4273eca2b5aa?s=96&d=mm&r=g\",\"contentUrl\":\"https:\/\/secure.gravatar.com\/avatar\/bb5b91fbdf9d62ff41ec4273eca2b5aa?s=96&d=mm&r=g\",\"caption\":\"Jane Tanner\"},\"url\":\"https:\/\/sites.exeter.ac.uk\/mathslocal\/author\/j-m-tannerexeter-ac-uk\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Workshop: Interactive Theorem Proving in Education and Research - Department of Maths and Stats local","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:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/","og_locale":"en_US","og_type":"article","og_title":"Workshop: Interactive Theorem Proving in Education and Research - Department of Maths and Stats local","og_description":"There will be a one-day workshop on 24 July 2024 and online, focused on how interactive theorem provers, like Lean and Isabelle, can be used in mathematics and computer science. This event is ideal for educators and researchers who use deductive proof. No prior experience is necessary: the day starts and ends with hands-on sessions [&hellip;]","og_url":"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/","og_site_name":"Department of Maths and Stats local","article_published_time":"2024-07-08T14:45:42+00:00","article_modified_time":"2024-07-08T16:01:21+00:00","author":"Jane Tanner","twitter_card":"summary_large_image","twitter_misc":{"Written by":"Jane Tanner"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/","url":"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/","name":"Workshop: Interactive Theorem Proving in Education and Research - Department of Maths and Stats local","isPartOf":{"@id":"https:\/\/sites.exeter.ac.uk\/mathslocal\/#website"},"datePublished":"2024-07-08T14:45:42+00:00","dateModified":"2024-07-08T16:01:21+00:00","author":{"@id":"https:\/\/sites.exeter.ac.uk\/mathslocal\/#\/schema\/person\/80ca16af2fbb5ea0718a2151f6973b7b"},"breadcrumb":{"@id":"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/sites.exeter.ac.uk\/mathslocal\/2024\/07\/08\/hello-world\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/sites.exeter.ac.uk\/mathslocal\/"},{"@type":"ListItem","position":2,"name":"Workshop: Interactive Theorem Proving in Education and Research"}]},{"@type":"WebSite","@id":"https:\/\/sites.exeter.ac.uk\/mathslocal\/#website","url":"https:\/\/sites.exeter.ac.uk\/mathslocal\/","name":"Department of Maths and Stats local","description":"","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/sites.exeter.ac.uk\/mathslocal\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"en-US"},{"@type":"Person","@id":"https:\/\/sites.exeter.ac.uk\/mathslocal\/#\/schema\/person\/80ca16af2fbb5ea0718a2151f6973b7b","name":"Jane Tanner","image":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/sites.exeter.ac.uk\/mathslocal\/#\/schema\/person\/image\/","url":"https:\/\/secure.gravatar.com\/avatar\/bb5b91fbdf9d62ff41ec4273eca2b5aa?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/bb5b91fbdf9d62ff41ec4273eca2b5aa?s=96&d=mm&r=g","caption":"Jane Tanner"},"url":"https:\/\/sites.exeter.ac.uk\/mathslocal\/author\/j-m-tannerexeter-ac-uk\/"}]}},"jetpack_sharing_enabled":true,"jetpack_featured_media_url":"","_links":{"self":[{"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/posts\/1"}],"collection":[{"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/comments?post=1"}],"version-history":[{"count":1,"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/posts\/1\/revisions"}],"predecessor-version":[{"id":57,"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/posts\/1\/revisions\/57"}],"wp:attachment":[{"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/media?parent=1"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/categories?post=1"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/sites.exeter.ac.uk\/mathslocal\/wp-json\/wp\/v2\/tags?post=1"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}