{"id":13518,"date":"2026-09-22T13:54:01","date_gmt":"2026-09-22T18:54:01","guid":{"rendered":"https:\/\/meetings.informs.org\/wordpress\/annual\/?page_id=13518"},"modified":"2026-09-22T13:55:10","modified_gmt":"2026-09-22T18:55:10","slug":"lean-formalization-agents","status":"publish","type":"page","link":"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/","title":{"rendered":"Lean Formalization Agents for Mathematics in Operations Research Workshop"},"content":{"rendered":"<!--themify_builder_content-->\n<div id=\"themify_builder_content-13518\" data-postid=\"13518\" class=\"themify_builder_content themify_builder_content-13518 themify_builder tf_clear\">\n                    <div  data-zoom-bg=\"desktop\" data-css_id=\"aewa994\" data-lazy=\"1\" class=\"module_row themify_builder_row fullwidth_row_container tb_aewa994 tb_first tf_w\">\n            <span  class=\"builder_row_cover tf_abs\" data-lazy=\"1\"><\/span>            <div class=\"row_inner col_align_top tb_col_count_1 tf_box tf_rel\">\n                        <div  data-lazy=\"1\" class=\"module_column tb-column col-full tb_qyp8994 first\">\n                    <!-- module text -->\n<div  class=\"module module-text tb_ipiq994   \" data-lazy=\"1\">\n        <div  class=\"tb_text_wrap\">\n        <h1>Lean Formalization Agents for Mathematics in Operations Research Workshop<\/h1>\n<p><strong>Saturday, October 31\u00a0 \u2022\u00a0 <\/strong><strong>3-5pm<\/strong><\/p>    <\/div>\n<\/div>\n<!-- \/module text -->        <\/div>\n                        <\/div>\n        <\/div>\n                        <div  data-lazy=\"1\" class=\"module_row themify_builder_row tb_9bwm798 tf_w\">\n                        <div class=\"row_inner col_align_top tb_col_count_1 tf_box tf_rel\">\n                        <div  data-lazy=\"1\" class=\"module_column tb-column col-full tb_nfa9798 first\">\n                            <div  data-lazy=\"1\" class=\"module_subrow themify_builder_sub_row tf_w col_align_top tb_col_count_1 tb_52pu798\">\n                <div  data-lazy=\"1\" class=\"module_column sub_column col-full tb_j9bo798 first\">\n                    <!-- module text -->\n<div  class=\"module module-text tb_kifa798   \" data-lazy=\"1\">\n        <div  class=\"tb_text_wrap\">\n        <p>This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology. The participants in the workshop will work with the agent, end-to-end, starting from a PDF version of a paper, and then producing a report, containing a diagram describing the mathematical results and statements, an assessment of what results are rigorously verified, which ones are repairable, and which results are not repairable (by providing a counter-example) or potentially very difficult to repair. If the paper is verifiable or repairable, the agent also provides a Lean formalized version of the results.<br \/><br \/><strong>Presenters<\/strong>: Guanting Chen, Xiaocheng Li, Shang Liu, and Jose Blanchet<\/p>\n<p><strong>Workshop Fee: $25<\/strong><\/p>\n<p><strong>All workshop participants are required to register for the 2026 INFORMS Annual Meeting in San Francisco.\u00a0<\/strong>The registration fee for this workshop does NOT include the registration fee for the INFORMS Annual Meeting.<\/p>    <\/div>\n<\/div>\n<!-- \/module text --><!-- module buttons -->\n<div  class=\"module module-buttons tb_vche67 buttons-horizontal solid  small circle\" data-lazy=\"1\">\n        <div class=\"module-buttons-item tf_in_flx\">\n                        <a href=\"https:\/\/meetings.informs.org\/wordpress\/annual\/register\/\" class=\"ui builder_button tf_in_flx light-green\" >\n                                                Click Here for Registration                                        <\/a>\n                <\/div>\n            <\/div>\n<!-- \/module buttons -->\n        <\/div>\n                    <\/div>\n                <\/div>\n                        <\/div>\n        <\/div>\n        <\/div>\n<!--\/themify_builder_content-->","protected":false},"excerpt":{"rendered":"<p>Lean Formalization Agents for Mathematics in Operations Research Workshop Saturday, October 31\u00a0 \u2022\u00a0 3-5pm<\/p>\n","protected":false},"author":46,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_acf_changed":false,"content-type":"","footnotes":""},"class_list":["post-13518","page","type-page","status-publish","hentry","has-post-title","has-post-date","has-post-category","has-post-tag","has-post-comment","has-post-author",""],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO Premium plugin v26.0 (Yoast SEO v26.0) - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>Lean Formalization Agents for Mathematics in Operations Research Workshop &#187; 2026 INFORMS Annual Meeting<\/title>\n<meta name=\"description\" content=\"This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology.\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Lean Formalization Agents for Mathematics in Operations Research Workshop\" \/>\n<meta property=\"og:description\" content=\"This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/\" \/>\n<meta property=\"og:site_name\" content=\"2026 INFORMS Annual Meeting\" \/>\n<meta property=\"article:modified_time\" content=\"2026-09-22T18:55:10+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/meetings.informs.org\/wordpress\/annual\/files\/2025\/10\/2026_INFORMS_Annual_Meeting_Logo.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"300\" \/>\n\t<meta property=\"og:image:height\" content=\"300\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"2 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/\",\"url\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/\",\"name\":\"Lean Formalization Agents for Mathematics in Operations Research Workshop &#187; 2026 INFORMS Annual Meeting\",\"isPartOf\":{\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/#website\"},\"datePublished\":\"2026-09-22T18:54:01+00:00\",\"dateModified\":\"2026-09-22T18:55:10+00:00\",\"description\":\"This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology.\",\"breadcrumb\":{\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Lean Formalization Agents for Mathematics in Operations Research Workshop\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/#website\",\"url\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/\",\"name\":\"2026 INFORMS Annual Meeting\",\"description\":\"November 1-4, 2026 | San Francisco, CA\",\"publisher\":{\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-US\"},{\"@type\":\"Organization\",\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/#organization\",\"name\":\"2026 INFORMS Annual Meeting\",\"url\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/#\/schema\/logo\/image\/\",\"url\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/files\/2025\/10\/cropped-2026_INFORMS_Annual_Meeting_Logo.png\",\"contentUrl\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/files\/2025\/10\/cropped-2026_INFORMS_Annual_Meeting_Logo.png\",\"width\":512,\"height\":512,\"caption\":\"2026 INFORMS Annual Meeting\"},\"image\":{\"@id\":\"https:\/\/meetings.informs.org\/wordpress\/annual\/#\/schema\/logo\/image\/\"}}]}<\/script>\n<!-- \/ Yoast SEO Premium plugin. -->","yoast_head_json":{"title":"Lean Formalization Agents for Mathematics in Operations Research Workshop &#187; 2026 INFORMS Annual Meeting","description":"This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology.","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:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/","og_locale":"en_US","og_type":"article","og_title":"Lean Formalization Agents for Mathematics in Operations Research Workshop","og_description":"This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology.","og_url":"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/","og_site_name":"2026 INFORMS Annual Meeting","article_modified_time":"2026-09-22T18:55:10+00:00","og_image":[{"width":300,"height":300,"url":"https:\/\/meetings.informs.org\/wordpress\/annual\/files\/2025\/10\/2026_INFORMS_Annual_Meeting_Logo.jpg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_misc":{"Est. reading time":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/","url":"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/","name":"Lean Formalization Agents for Mathematics in Operations Research Workshop &#187; 2026 INFORMS Annual Meeting","isPartOf":{"@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/#website"},"datePublished":"2026-09-22T18:54:01+00:00","dateModified":"2026-09-22T18:55:10+00:00","description":"This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology.","breadcrumb":{"@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/lean-formalization-agents\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/meetings.informs.org\/wordpress\/annual\/"},{"@type":"ListItem","position":2,"name":"Lean Formalization Agents for Mathematics in Operations Research Workshop"}]},{"@type":"WebSite","@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/#website","url":"https:\/\/meetings.informs.org\/wordpress\/annual\/","name":"2026 INFORMS Annual Meeting","description":"November 1-4, 2026 | San Francisco, CA","publisher":{"@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/meetings.informs.org\/wordpress\/annual\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-US"},{"@type":"Organization","@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/#organization","name":"2026 INFORMS Annual Meeting","url":"https:\/\/meetings.informs.org\/wordpress\/annual\/","logo":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/#\/schema\/logo\/image\/","url":"https:\/\/meetings.informs.org\/wordpress\/annual\/files\/2025\/10\/cropped-2026_INFORMS_Annual_Meeting_Logo.png","contentUrl":"https:\/\/meetings.informs.org\/wordpress\/annual\/files\/2025\/10\/cropped-2026_INFORMS_Annual_Meeting_Logo.png","width":512,"height":512,"caption":"2026 INFORMS Annual Meeting"},"image":{"@id":"https:\/\/meetings.informs.org\/wordpress\/annual\/#\/schema\/logo\/image\/"}}]}},"builder_content":"<h1>Lean Formalization Agents for Mathematics in Operations Research Workshop<\/h1> <p><strong>Saturday, October 31\u00a0 \u2022\u00a0 <\/strong><strong>3-5pm<\/strong><\/p>\n<p>This workshop will introduce an agent that verifies and formalizes mathematical papers that are focused on Operations Research mathematical methodology. The participants in the workshop will work with the agent, end-to-end, starting from a PDF version of a paper, and then producing a report, containing a diagram describing the mathematical results and statements, an assessment of what results are rigorously verified, which ones are repairable, and which results are not repairable (by providing a counter-example) or potentially very difficult to repair. If the paper is verifiable or repairable, the agent also provides a Lean formalized version of the results.<br \/><br \/><strong>Presenters<\/strong>: Guanting Chen, Xiaocheng Li, Shang Liu, and Jose Blanchet<\/p> <p><strong>Workshop Fee: $25<\/strong><\/p> <p><strong>All workshop participants are required to register for the 2026 INFORMS Annual Meeting in San Francisco.\u00a0<\/strong>The registration fee for this workshop does NOT include the registration fee for the INFORMS Annual Meeting.<\/p>\n<a href=\"https:\/\/meetings.informs.org\/wordpress\/annual\/register\/\" > Click Here for Registration <\/a>","_links":{"self":[{"href":"https:\/\/meetings.informs.org\/wordpress\/annual\/wp-json\/wp\/v2\/pages\/13518","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/meetings.informs.org\/wordpress\/annual\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/meetings.informs.org\/wordpress\/annual\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/meetings.informs.org\/wordpress\/annual\/wp-json\/wp\/v2\/users\/46"}],"replies":[{"embeddable":true,"href":"https:\/\/meetings.informs.org\/wordpress\/annual\/wp-json\/wp\/v2\/comments?post=13518"}],"version-history":[{"count":4,"href":"https:\/\/meetings.informs.org\/wordpress\/annual\/wp-json\/wp\/v2\/pages\/13518\/revisions"}],"predecessor-version":[{"id":13522,"href":"https:\/\/meetings.informs.org\/wordpress\/annual\/wp-json\/wp\/v2\/pages\/13518\/revisions\/13522"}],"wp:attachment":[{"href":"https:\/\/meetings.informs.org\/wordpress\/annual\/wp-json\/wp\/v2\/media?parent=13518"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}