{"id":23379,"date":"2026-02-04T11:53:42","date_gmt":"2026-02-04T16:53:42","guid":{"rendered":"https:\/\/carleton.ca\/scs\/?post_type=cu-events&#038;p=23379"},"modified":"2026-02-04T11:53:42","modified_gmt":"2026-02-04T16:53:42","slug":"school-colloquium-by-dr-kevin-cheung","status":"publish","type":"cu-events","link":"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/","title":{"rendered":"School Colloquium by Dr. Kevin Cheung"},"content":{"rendered":"<p data-start=\"1254\" data-end=\"1357\"><strong data-start=\"1254\" data-end=\"1357\">The School of Mathematics and Statistics will be holding a Colloquium on Friday, February 13, 2026.<\/strong><\/p>\n<ul>\n<li data-start=\"1362\" data-end=\"1700\"><strong data-start=\"1362\" data-end=\"1372\">Title:<\/strong> Leaning Towards Formal Proofs<\/li>\n<li data-start=\"1362\" data-end=\"1700\"><strong data-start=\"1407\" data-end=\"1419\">Speaker:<\/strong> <a href=\"https:\/\/carleton.ca\/math\/people\/kevin-cheung\/\">Dr. Kevin Cheung<\/a>, School of Mathematics and Statistics, Carleton University<\/li>\n<li data-start=\"1362\" data-end=\"1700\"><strong data-start=\"1705\" data-end=\"1718\">Abstract: <\/strong>In recent years, there has been increasing interest among mathematicians in using the Lean interactive theorem prover to develop formal proofs. In this talk, I will give a brief introduction to Lean and share some personal experiences using the system.<\/li>\n<\/ul>\n","protected":false},"template":"","meta":{"_relevanssi_hide_post":"","_relevanssi_hide_content":"","_relevanssi_pin_for_all":"","_relevanssi_pin_keywords":"","_relevanssi_unpin_keywords":"","_relevanssi_related_keywords":"","_relevanssi_related_include_ids":"","_relevanssi_related_exclude_ids":"","_relevanssi_related_no_append":"","_relevanssi_related_not_related":"","_relevanssi_related_posts":"","_relevanssi_noindex_reason":"","_mi_skip_tracking":false,"_exactmetrics_sitenote_active":false,"_exactmetrics_sitenote_note":"","_exactmetrics_sitenote_category":0,"_links_to":"","_links_to_target":""},"daevent-type":[100],"event-audience":[],"event-featured":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v21.2 - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>School Colloquium by Dr. Kevin Cheung - Events - School of Computer Science<\/title>\n<meta name=\"description\" content=\"The School of Mathematics and Statistics will be holding a Colloquium on Friday, February 13, 2026. Title: Leaning Towards Formal Proofs Speaker: Dr.\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/\" \/>\n<meta name=\"twitter:label1\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"1 minute\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/\",\"url\":\"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/\",\"name\":\"School Colloquium by Dr. Kevin Cheung - Events - School of Computer Science\",\"isPartOf\":{\"@id\":\"https:\/\/carleton.ca\/scs\/#website\"},\"datePublished\":\"2026-02-04T16:53:42+00:00\",\"dateModified\":\"2026-02-04T16:53:42+00:00\",\"description\":\"The School of Mathematics and Statistics will be holding a Colloquium on Friday, February 13, 2026. Title: Leaning Towards Formal Proofs Speaker: Dr.\",\"breadcrumb\":{\"@id\":\"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/carleton.ca\/scs\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Events\",\"item\":\"https:\/\/carleton.ca\/scs\/cu-events\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"School Colloquium by Dr. Kevin Cheung\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/carleton.ca\/scs\/#website\",\"url\":\"https:\/\/carleton.ca\/scs\/\",\"name\":\"School of Computer Science\",\"description\":\"Carleton University\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/carleton.ca\/scs\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"en-US\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"School Colloquium by Dr. Kevin Cheung - Events - School of Computer Science","description":"The School of Mathematics and Statistics will be holding a Colloquium on Friday, February 13, 2026. Title: Leaning Towards Formal Proofs Speaker: Dr.","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:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/","twitter_misc":{"Est. reading time":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/","url":"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/","name":"School Colloquium by Dr. Kevin Cheung - Events - School of Computer Science","isPartOf":{"@id":"https:\/\/carleton.ca\/scs\/#website"},"datePublished":"2026-02-04T16:53:42+00:00","dateModified":"2026-02-04T16:53:42+00:00","description":"The School of Mathematics and Statistics will be holding a Colloquium on Friday, February 13, 2026. Title: Leaning Towards Formal Proofs Speaker: Dr.","breadcrumb":{"@id":"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/carleton.ca\/scs\/cu-events\/school-colloquium-by-dr-kevin-cheung\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/carleton.ca\/scs\/"},{"@type":"ListItem","position":2,"name":"Events","item":"https:\/\/carleton.ca\/scs\/cu-events\/"},{"@type":"ListItem","position":3,"name":"School Colloquium by Dr. Kevin Cheung"}]},{"@type":"WebSite","@id":"https:\/\/carleton.ca\/scs\/#website","url":"https:\/\/carleton.ca\/scs\/","name":"School of Computer Science","description":"Carleton University","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/carleton.ca\/scs\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"en-US"}]}},"acf":{"Date":"2026.02.13","Start Time":"15:30","End Time":"16:30","Multi Day Event":"","Location: Building":"herzberg","Location: Room":"HP 4351, Macphail Room, Herzberg Building, 4th floor","show_cost":"no","audience":false,"Contact Name":"","Contact Email":"","Contact Phone":"","More Info Link":""},"_links":{"self":[{"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/cu-events\/23379"}],"collection":[{"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/cu-events"}],"about":[{"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/types\/cu-events"}],"version-history":[{"count":4,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/cu-events\/23379\/revisions"}],"predecessor-version":[{"id":23389,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/cu-events\/23379\/revisions\/23389"}],"wp:attachment":[{"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/media?parent=23379"}],"wp:term":[{"taxonomy":"daevent-type","embeddable":true,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/daevent-type?post=23379"},{"taxonomy":"event-audience","embeddable":true,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/event-audience?post=23379"},{"taxonomy":"event-featured","embeddable":true,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/event-featured?post=23379"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}