{"id":513,"date":"2019-09-04T16:02:24","date_gmt":"2019-09-04T16:02:24","guid":{"rendered":"https:\/\/website.prod.unilu.spikeseed.cloud\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/"},"modified":"2019-09-04T16:02:24","modified_gmt":"2019-09-04T16:02:24","slug":"world-championship-in-automated-reasoning-computer-scientist-awarded","status":"publish","type":"news","link":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/","title":{"rendered":"World-championship in Automated Reasoning: computer scientist awarded"},"content":{"rendered":"<section class=\"wp-block-unilux-blocks-free-section section\"><div class=\"container xl:max-w-screen-xl\"><p>On the occasion of the annual World Championship for Automatic Theorem Proving (\u201cCADE ATP System Competition\u201d, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for \u201cLeo-III\u201d, a computer software that proves mathematical conjectures autonomously.<\/p><p><strong>Automatic reasoning<\/strong><\/p><p>Leo-III has been developed since 2014 by Alexander Steen, post-doc researcher within the Computer Science and Communications Research Unit (<a href=\"https:\/\/wwwfr.uni.lu\/recherche\/fstm\/dcs\" target=\"_self\" title=\"\" rel=\"noopener\">CSC<\/a>) at the University of Luxembourg. \u201cLeo-III is a computer software that we call \u00ab\u00a0automated theorem prover\u00a0\u00bb or, more general, a reasoning system that tries to find proofs for mathematical conjectures completely autonomously, that is without any help or advice from humans. The input of such systems is a problem statement in a formal logical language, and the output is &#8212; if successful \u2013 a formal proof of that conjecture\u201d, explains Alexander.<\/p><figure class=\"wp-block-dev4-reusable-blocks-image  object-fit--contain\">\n    \n<img decoding=\"async\" class=\"wp-block-image unilux-custom-image-block\"\n                alt=\"\"\n            src=\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2023\/07\/img_3345-rotated.jpg\"\n                    style=\"object-position: 50.00% 50.00%; font-family: &quot;object-fit: contain; object-position: 50.00% 50.00%;&quot;; aspect-ratio: 4\/3; object-fit: contain; width: 100%;\"\n        loading=\"lazy\"\n\/>    <\/figure><p><strong>Applications in mathematics and beyond<\/strong><\/p><p>Theorem provers are used by mathematicians and computer scientists to formalise and to find proofs. In the first case, the human can input a proof of a mathematical statement and the system will check it for correctness; in the latter case, the proof is generated by the system in full.<\/p><p>Specifically, Leo-III automated a logical language which is referred to as \u00ab\u00a0higher-order logic\u00a0\u00bb, which is a very expressive formalism that can capture even more applications; but is also harder to realise in practice. Recently,\u00a0<a href=\"https:\/\/wwwfr.uni.lu\/recherche\/fstm\/dcs\/members\/christoph_ewald_benzmueller\" target=\"_self\" title=\"\" rel=\"noopener\">Christoph Benzm\u00fcller<\/a>, Professor at Freie Universit\u00e4t Berlin, Germany, and affiliated with the University of Luxembourg, has applied such systems to assess e.g. philosophical arguments from metaphysics.<\/p><p>\u201cI am currently working on applying this technology to reasoning in the context of computer ethics and normative applications. With this step, of course, the target audience will eventually be even wider than just mathematicians and computer scientists\u201d, adds Alexander.<\/p><p><strong>International recognition<\/strong><\/p><p>Leo-III ranked first place in the category \u00ab\u00a0Large Theory Batch\u00a0\u00bb (LTB) during the annual <a href=\"http:\/\/www.tptp.org\/CASC\/\" target=\"_blank\" title=\"\" rel=\"noopener\">World Championship for Automatic Theorem Proving<\/a> with over 54% solved problems (5441 out of 10000). \u201cI am very happy about the good performance that Leo-III demonstrated in the LTB category, that has classically been dominated by first-order provers in the last years. This is a strong indication that the extra efforts of automating higher-order logic come with convincing benefits in practical applications\u201d. The next best systems, the world leading first-order provers E (DHBW Stuttgart) and Vampire (U Manchester) found roughly 15% and 17% less solutions, respectively. Leo-III also ranked second place in the smaller THF division.<\/p><p>Leo-III is open-source software and freely available for use and further development. Details on the system and its theoretical foundations can be found in Steen\u2019s PhD thesis.\u00a0<\/p><p>More information: <a href=\"http:\/\/page.mi.fu-berlin.de\/lex\/leo3\/\" target=\"_blank\" title=\"\" rel=\"noopener\">http:\/\/page.mi.fu-berlin.de\/lex\/leo3\/<\/a><\/p><\/div><\/section>","protected":false},"excerpt":{"rendered":"<p>On the occasion of the annual World Championship for Automatic Theorem Proving (\u201cCADE ATP System Competition\u201d, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for \u201cLeo-III\u201d, a computer software that proves mathematical conjectures autonomously.<\/p>\n","protected":false},"author":0,"featured_media":0,"template":"","format":"standard","meta":{"featured_image_focal_point":[],"show_featured_caption":false,"ulux_newsletter_groups":"","uluxPostTitle":"","uluxPrePostTitle":"","_trash_the_other_posts":false,"_price":"","_stock":"","_tribe_ticket_header":"","_tribe_default_ticket_provider":"","_tribe_ticket_capacity":"0","_ticket_start_date":"","_ticket_end_date":"","_tribe_ticket_show_description":"","_tribe_ticket_show_not_going":false,"_tribe_ticket_use_global_stock":"","_tribe_ticket_global_stock_level":"","_global_stock_mode":"","_global_stock_cap":"","_tribe_rsvp_for_event":"","_tribe_ticket_going_count":"","_tribe_ticket_not_going_count":"","_tribe_tickets_list":"[]","_tribe_ticket_has_attendee_info_fields":false},"news-category":[3],"news-topic":[],"organisation":[25,226],"authorship":[],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO Premium plugin v22.3 (Yoast SEO v22.3) - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>World-championship in Automated Reasoning: computer scientist awarded - Universit\u00e9 du Luxembourg<\/title>\n<meta name=\"description\" content=\"On the occasion of the annual World Championship for Automatic Theorem Proving (\u201cCADE ATP System Competition\u201d, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for \u201cLeo-III\u201d, a computer software that proves mathematical conjectures autonomously.\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/\" \/>\n<meta property=\"og:locale\" content=\"fr_FR\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"World-championship in Automated Reasoning: computer scientist awarded\" \/>\n<meta property=\"og:description\" content=\"On the occasion of the annual World Championship for Automatic Theorem Proving (\u201cCADE ATP System Competition\u201d, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for \u201cLeo-III\u201d, a computer software that proves mathematical conjectures autonomously.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/\" \/>\n<meta property=\"og:site_name\" content=\"UNI FR\" \/>\n<meta property=\"article:publisher\" content=\"https:\/\/www.facebook.com\/uni.lu\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"2560\" \/>\n\t<meta property=\"og:image:height\" content=\"2560\" \/>\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=\"Dur\u00e9e de lecture estim\u00e9e\" \/>\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\":\"NewsArticle\",\"@id\":\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/#article\",\"isPartOf\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/\"},\"author\":{\"name\":\"\",\"@id\":\"\"},\"headline\":\"World-championship in Automated Reasoning: computer scientist awarded\",\"datePublished\":\"2019-09-04T16:02:24+00:00\",\"dateModified\":\"2019-09-04T16:02:24+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/\"},\"wordCount\":449,\"publisher\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/#organization\"},\"inLanguage\":\"fr-FR\"},{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/\",\"url\":\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/\",\"name\":\"World-championship in Automated Reasoning: computer scientist awarded - Universit\u00e9 du Luxembourg\",\"isPartOf\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/#website\"},\"datePublished\":\"2019-09-04T16:02:24+00:00\",\"dateModified\":\"2019-09-04T16:02:24+00:00\",\"description\":\"On the occasion of the annual World Championship for Automatic Theorem Proving (\u201cCADE ATP System Competition\u201d, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for \u201cLeo-III\u201d, a computer software that proves mathematical conjectures autonomously.\",\"breadcrumb\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/#breadcrumb\"},\"inLanguage\":\"fr-FR\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/www.uni.lu\/fr\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"News\",\"item\":\"https:\/\/www.uni.lu\/fr\/news\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"World-championship in Automated Reasoning: computer scientist awarded\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.uni.lu\/fr\/#website\",\"url\":\"https:\/\/www.uni.lu\/fr\/\",\"name\":\"Uni.lu\",\"description\":\"Universit\u00e9 du Luxembourg\",\"publisher\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/#organization\"},\"alternateName\":\"Universit\u00e9 du Luxembourg\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/www.uni.lu\/fr\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"fr-FR\"},{\"@type\":\"Organization\",\"@id\":\"https:\/\/www.uni.lu\/fr\/#organization\",\"name\":\"Universit\u00e9 du Luxembourg\",\"alternateName\":\"Uni.lu\",\"url\":\"https:\/\/www.uni.lu\/fr\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"fr-FR\",\"@id\":\"https:\/\/www.uni.lu\/fr\/#\/schema\/logo\/image\/\",\"url\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg\",\"contentUrl\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg\",\"width\":2560,\"height\":2560,\"caption\":\"Universit\u00e9 du Luxembourg\"},\"image\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/#\/schema\/logo\/image\/\"},\"sameAs\":[\"https:\/\/www.facebook.com\/uni.lu\",\"https:\/\/www.linkedin.com\/school\/university-of-luxembourg\/\",\"https:\/\/www.instagram.com\/uni.lu\",\"https:\/\/www.youtube.com\/@uni_lu\",\"https:\/\/en.wikipedia.org\/wiki\/University_of_Luxembourg\"],\"description\":\"Universit\u00e9 du Luxembourg\"}]}<\/script>\n<!-- \/ Yoast SEO Premium plugin. -->","yoast_head_json":{"title":"World-championship in Automated Reasoning: computer scientist awarded - Universit\u00e9 du Luxembourg","description":"On the occasion of the annual World Championship for Automatic Theorem Proving (\u201cCADE ATP System Competition\u201d, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for \u201cLeo-III\u201d, a computer software that proves mathematical conjectures autonomously.","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:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/","og_locale":"fr_FR","og_type":"article","og_title":"World-championship in Automated Reasoning: computer scientist awarded","og_description":"On the occasion of the annual World Championship for Automatic Theorem Proving (\u201cCADE ATP System Competition\u201d, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for \u201cLeo-III\u201d, a computer software that proves mathematical conjectures autonomously.","og_url":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/","og_site_name":"UNI FR","article_publisher":"https:\/\/www.facebook.com\/uni.lu","og_image":[{"width":2560,"height":2560,"url":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_misc":{"Dur\u00e9e de lecture estim\u00e9e":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"NewsArticle","@id":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/#article","isPartOf":{"@id":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/"},"author":{"name":"","@id":""},"headline":"World-championship in Automated Reasoning: computer scientist awarded","datePublished":"2019-09-04T16:02:24+00:00","dateModified":"2019-09-04T16:02:24+00:00","mainEntityOfPage":{"@id":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/"},"wordCount":449,"publisher":{"@id":"https:\/\/www.uni.lu\/fr\/#organization"},"inLanguage":"fr-FR"},{"@type":"WebPage","@id":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/","url":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/","name":"World-championship in Automated Reasoning: computer scientist awarded - Universit\u00e9 du Luxembourg","isPartOf":{"@id":"https:\/\/www.uni.lu\/fr\/#website"},"datePublished":"2019-09-04T16:02:24+00:00","dateModified":"2019-09-04T16:02:24+00:00","description":"On the occasion of the annual World Championship for Automatic Theorem Proving (\u201cCADE ATP System Competition\u201d, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for \u201cLeo-III\u201d, a computer software that proves mathematical conjectures autonomously.","breadcrumb":{"@id":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/#breadcrumb"},"inLanguage":"fr-FR","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.uni.lu\/fr\/news\/world-championship-in-automated-reasoning-computer-scientist-awarded\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.uni.lu\/fr\/"},{"@type":"ListItem","position":2,"name":"News","item":"https:\/\/www.uni.lu\/fr\/news\/"},{"@type":"ListItem","position":3,"name":"World-championship in Automated Reasoning: computer scientist awarded"}]},{"@type":"WebSite","@id":"https:\/\/www.uni.lu\/fr\/#website","url":"https:\/\/www.uni.lu\/fr\/","name":"Uni.lu","description":"Universit\u00e9 du Luxembourg","publisher":{"@id":"https:\/\/www.uni.lu\/fr\/#organization"},"alternateName":"Universit\u00e9 du Luxembourg","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.uni.lu\/fr\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"fr-FR"},{"@type":"Organization","@id":"https:\/\/www.uni.lu\/fr\/#organization","name":"Universit\u00e9 du Luxembourg","alternateName":"Uni.lu","url":"https:\/\/www.uni.lu\/fr\/","logo":{"@type":"ImageObject","inLanguage":"fr-FR","@id":"https:\/\/www.uni.lu\/fr\/#\/schema\/logo\/image\/","url":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg","contentUrl":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg","width":2560,"height":2560,"caption":"Universit\u00e9 du Luxembourg"},"image":{"@id":"https:\/\/www.uni.lu\/fr\/#\/schema\/logo\/image\/"},"sameAs":["https:\/\/www.facebook.com\/uni.lu","https:\/\/www.linkedin.com\/school\/university-of-luxembourg\/","https:\/\/www.instagram.com\/uni.lu","https:\/\/www.youtube.com\/@uni_lu","https:\/\/en.wikipedia.org\/wiki\/University_of_Luxembourg"],"description":"Universit\u00e9 du Luxembourg"}]}},"blog_id":11,"_links":{"self":[{"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/news\/513"}],"collection":[{"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/news"}],"about":[{"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/types\/news"}],"version-history":[{"count":0,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/news\/513\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/media?parent=513"}],"wp:term":[{"taxonomy":"news-category","embeddable":true,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/news-category?post=513"},{"taxonomy":"news-topic","embeddable":true,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/news-topic?post=513"},{"taxonomy":"organisation","embeddable":true,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/organisation?post=513"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}