CINXE.COM

<!DOCTYPE html> <html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available" lang="en" dir="ltr"> <head> <meta charset="UTF-8"> <title>Lean (proof assistant) - Wikipedia</title> <script>(function(){var className="client-js vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available";var cookie=document.cookie.match(/(?:^|; )enwikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":["",""],"wgDigitTransformTable":["",""],"wgDefaultDateFormat":"dmy", "wgMonthNames":["","January","February","March","April","May","June","July","August","September","October","November","December"],"wgRequestId":"a0609867-f4b4-4336-84e3-2c85d55e1106","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Lean_(proof_assistant)","wgTitle":"Lean (proof assistant)","wgCurRevisionId":1254178588,"wgRevisionId":1254178588,"wgArticleId":62889984,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Articles with short description","Short description is different from Wikidata","All articles with unsourced statements","Articles with unsourced statements from October 2023","Programming languages created in 2013","Proof assistants","Dependently typed languages","Educational math software","Functional languages","Free and open-source software","Free software programmed in C++","Microsoft free software","Microsoft programming languages","Microsoft Research", "Software using the Apache license","Free mathematics software","Theorem proving software systems"],"wgPageViewLanguage":"en","wgPageContentLanguage":"en","wgPageContentModel":"wikitext","wgRelevantPageName":"Lean_(proof_assistant)","wgRelevantArticleId":62889984,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia","wgCiteReferencePreviewsActive":false,"wgFlaggedRevsParams":{"tags":{"status":{"levels":1}}},"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"en","pageLanguageDir":"ltr","pageVariantFallbacks":"en"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":false,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":20000,"wgRelatedArticlesCompat":[],"wgCentralAuthMobileDomain":false,"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage", "wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q6509476","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"],"GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false,"wgGELevelingUpEnabledForUser":false};RLSTATE={"ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.cite.styles":"ready","ext.pygments":"ready","ext.math.styles":"ready","skins.vector.search.codex.styles":"ready","skins.vector.styles":"ready","skins.vector.icons":"ready","jquery.makeCollapsible.styles":"ready","ext.wikimediamessages.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready", "ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","ext.pygments.view","site","mediawiki.page.ready","jquery.makeCollapsible","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ReferenceTooltips","ext.gadget.switcher","ext.urlShortener.toolbar","ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init","ext.visualEditor.targetLoader","ext.echo.centralauth","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.interface","ext.cx.eventlogging.campaigns","ext.cx.uls.quick.actions","wikibase.client.vector-2022","ext.checkUser.clientHints","ext.growthExperiments.SuggestedEditSession","wikibase.sidebar.tracking"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=en&modules=ext.cite.styles%7Cext.math.styles%7Cext.pygments%2CwikimediaBadges%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediamessages.styles%7Cjquery.makeCollapsible.styles%7Cskins.vector.icons%2Cstyles%7Cskins.vector.search.codex.styles%7Cwikibase.client.init&only=styles&skin=vector-2022"> <script async="" src="/w/load.php?lang=en&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=en&modules=site.styles&only=styles&skin=vector-2022"> <meta name="generator" content="MediaWiki 1.44.0-wmf.4"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="Lean (proof assistant) - Wikipedia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//en.m.wikipedia.org/wiki/Lean_(proof_assistant)"> <link rel="alternate" type="application/x-wiki" title="Edit this page" href="/w/index.php?title=Lean_(proof_assistant)&action=edit"> <link rel="apple-touch-icon" href="/static/apple-touch/wikipedia.png"> <link rel="icon" href="/static/favicon/wikipedia.ico"> <link rel="search" type="application/opensearchdescription+xml" href="/w/rest.php/v1/search" title="Wikipedia (en)"> <link rel="EditURI" type="application/rsd+xml" href="//en.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://en.wikipedia.org/wiki/Lean_(proof_assistant)"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en"> <link rel="alternate" type="application/atom+xml" title="Wikipedia Atom feed" href="/w/index.php?title=Special:RecentChanges&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="//login.wikimedia.org"> </head> <body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-Lean_proof_assistant rootpage-Lean_proof_assistant skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Jump to content</a> <div class="vector-header-container"> <header class="vector-header mw-header"> <div class="vector-header-start"> <nav class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-dropdown" class="vector-dropdown vector-main-menu-dropdown vector-button-flush-left vector-button-flush-right" > <input type="checkbox" id="vector-main-menu-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-main-menu-dropdown" class="vector-dropdown-checkbox " aria-label="Main menu" > <label id="vector-main-menu-dropdown-label" for="vector-main-menu-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-menu mw-ui-icon-wikimedia-menu"></span> <span class="vector-dropdown-label-text">Main menu</span> </label> <div class="vector-dropdown-content"> <div id="vector-main-menu-unpinned-container" class="vector-unpinned-container"> <div id="vector-main-menu" class="vector-main-menu vector-pinnable-element"> <div class="vector-pinnable-header vector-main-menu-pinnable-header vector-pinnable-header-unpinned" data-feature-name="main-menu-pinned" data-pinnable-element-id="vector-main-menu" data-pinned-container-id="vector-main-menu-pinned-container" data-unpinned-container-id="vector-main-menu-unpinned-container" > <div class="vector-pinnable-header-label">Main menu</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">hide</button> </div> <div id="p-navigation" class="vector-menu mw-portlet mw-portlet-navigation" > <div class="vector-menu-heading"> Navigation </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Main_Page" title="Visit the main page [z]" accesskey="z"><span>Main page</span></a></li><li id="n-contents" class="mw-list-item"><a href="/wiki/Wikipedia:Contents" title="Guides to browsing Wikipedia"><span>Contents</span></a></li><li id="n-currentevents" class="mw-list-item"><a href="/wiki/Portal:Current_events" title="Articles related to current events"><span>Current events</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Special:Random" title="Visit a randomly selected article [x]" accesskey="x"><span>Random article</span></a></li><li id="n-aboutsite" class="mw-list-item"><a href="/wiki/Wikipedia:About" title="Learn about Wikipedia and how it works"><span>About Wikipedia</span></a></li><li id="n-contactpage" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us" title="How to contact Wikipedia"><span>Contact us</span></a></li> </ul> </div> </div> <div id="p-interaction" class="vector-menu mw-portlet mw-portlet-interaction" > <div class="vector-menu-heading"> Contribute </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-help" class="mw-list-item"><a href="/wiki/Help:Contents" title="Guidance on how to use and edit Wikipedia"><span>Help</span></a></li><li id="n-introduction" class="mw-list-item"><a href="/wiki/Help:Introduction" title="Learn how to edit Wikipedia"><span>Learn to edit</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikipedia:Community_portal" title="The hub for editors"><span>Community portal</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Special:RecentChanges" title="A list of recent changes to Wikipedia [r]" accesskey="r"><span>Recent changes</span></a></li><li id="n-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_upload_wizard" title="Add images or other media for use on Wikipedia"><span>Upload file</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Main_Page" class="mw-logo"> <img class="mw-logo-icon" src="/static/images/icons/wikipedia.png" alt="" aria-hidden="true" height="50" width="50"> <span class="mw-logo-container skin-invert"> <img class="mw-logo-wordmark" alt="Wikipedia" src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" style="width: 7.5em; height: 1.125em;"> <img class="mw-logo-tagline" alt="The Free Encyclopedia" src="/static/images/mobile/copyright/wikipedia-tagline-en.svg" width="117" height="13" style="width: 7.3125em; height: 0.8125em;"> </span> </a> </div> <div class="vector-header-end"> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-collapses vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <a href="/wiki/Special:Search" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Search Wikipedia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </a> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail cdx-typeahead-search--auto-expand-width"> <form action="/w/index.php" id="searchform" class="cdx-search-input cdx-search-input--has-end-button"> <div id="simpleSearch" class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia" aria-label="Search Wikipedia" autocapitalize="sentences" title="Search Wikipedia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Personal tools"> <div class="vector-user-links-main"> <div id="p-vector-user-menu-preferences" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-userpage" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Change the appearance of the page's font size, width, and color" > <input type="checkbox" id="vector-appearance-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-appearance-dropdown" class="vector-dropdown-checkbox " aria-label="Appearance" > <label id="vector-appearance-dropdown-label" for="vector-appearance-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-appearance mw-ui-icon-wikimedia-appearance"></span> <span class="vector-dropdown-label-text">Appearance</span> </label> <div class="vector-dropdown-content"> <div id="vector-appearance-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div id="p-vector-user-menu-notifications" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-overflow" class="vector-menu mw-portlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en" class=""><span>Donate</span></a> </li> <li id="pt-createaccount-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:CreateAccount&returnto=Lean+%28proof+assistant%29" title="You are encouraged to create an account and log in; however, it is not mandatory" class=""><span>Create account</span></a> </li> <li id="pt-login-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:UserLogin&returnto=Lean+%28proof+assistant%29" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o" class=""><span>Log in</span></a> </li> </ul> </div> </div> </div> <div id="vector-user-links-dropdown" class="vector-dropdown vector-user-menu vector-button-flush-right vector-user-menu-logged-out" title="Log in and more options" > <input type="checkbox" id="vector-user-links-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-user-links-dropdown" class="vector-dropdown-checkbox " aria-label="Personal tools" > <label id="vector-user-links-dropdown-label" for="vector-user-links-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-ellipsis mw-ui-icon-wikimedia-ellipsis"></span> <span class="vector-dropdown-label-text">Personal tools</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="User menu" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport" class="user-links-collapsible-item mw-list-item"><a href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en"><span>Donate</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:CreateAccount&returnto=Lean+%28proof+assistant%29" title="You are encouraged to create an account and log in; however, it is not mandatory"><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Create account</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:UserLogin&returnto=Lean+%28proof+assistant%29" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Log in</span></a></li> </ul> </div> </div> <div id="p-user-menu-anon-editor" class="vector-menu mw-portlet mw-portlet-user-menu-anon-editor" > <div class="vector-menu-heading"> Pages for logged out editors <a href="/wiki/Help:Introduction" aria-label="Learn more about editing"><span>learn more</span></a> </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Special:MyContributions" title="A list of edits made from this IP address [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Special:MyTalk" title="Discussion about edits from this IP address [n]" accesskey="n"><span>Talk</span></a></li> </ul> </div> </div> </div> </div> </nav> </div> </header> </div> <div class="mw-page-container"> <div class="mw-page-container-inner"> <div class="vector-sitenotice-container"> <div id="siteNotice"></div> </div> <div class="vector-column-start"> <div class="vector-main-menu-container"> <div id="mw-navigation"> <nav id="mw-panel" class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-pinned-container" class="vector-pinned-container"> </div> </nav> </div> </div> <div class="vector-sticky-pinned-container"> <nav id="mw-panel-toc" aria-label="Contents" data-event-name="ui.sidebar-toc" class="mw-table-of-contents-container vector-toc-landmark"> <div id="vector-toc-pinned-container" class="vector-pinned-container"> <div id="vector-toc" class="vector-toc vector-pinnable-element"> <div class="vector-pinnable-header vector-toc-pinnable-header vector-pinnable-header-pinned" data-feature-name="toc-pinned" data-pinnable-element-id="vector-toc" > <h2 class="vector-pinnable-header-label">Contents</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">hide</button> </div> <ul class="vector-toc-contents" id="mw-panel-toc-list"> <li id="toc-mw-content-text" class="vector-toc-list-item vector-toc-level-1"> <a href="#" class="vector-toc-link"> <div class="vector-toc-text">(Top)</div> </a> </li> <li id="toc-History" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#History"> <div class="vector-toc-text"> <span class="vector-toc-numb">1</span> <span>History</span> </div> </a> <ul id="toc-History-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Overview" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Overview"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>Overview</span> </div> </a> <button aria-controls="toc-Overview-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle Overview subsection</span> </button> <ul id="toc-Overview-sublist" class="vector-toc-list"> <li id="toc-Libraries" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Libraries"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.1</span> <span>Libraries</span> </div> </a> <ul id="toc-Libraries-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Editors_integration" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Editors_integration"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.2</span> <span>Editors integration</span> </div> </a> <ul id="toc-Editors_integration-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Examples_(Lean_4)" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Examples_(Lean_4)"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>Examples (Lean 4)</span> </div> </a> <ul id="toc-Examples_(Lean_4)-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Usage" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Usage"> <div class="vector-toc-text"> <span class="vector-toc-numb">4</span> <span>Usage</span> </div> </a> <button aria-controls="toc-Usage-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle Usage subsection</span> </button> <ul id="toc-Usage-sublist" class="vector-toc-list"> <li id="toc-Mathematics" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Mathematics"> <div class="vector-toc-text"> <span class="vector-toc-numb">4.1</span> <span>Mathematics</span> </div> </a> <ul id="toc-Mathematics-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Artificial_intelligence" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Artificial_intelligence"> <div class="vector-toc-text"> <span class="vector-toc-numb">4.2</span> <span>Artificial intelligence</span> </div> </a> <ul id="toc-Artificial_intelligence-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-See_also" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#See_also"> <div class="vector-toc-text"> <span class="vector-toc-numb">5</span> <span>See also</span> </div> </a> <ul id="toc-See_also-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-References" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#References"> <div class="vector-toc-text"> <span class="vector-toc-numb">6</span> <span>References</span> </div> </a> <ul id="toc-References-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-External_links" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#External_links"> <div class="vector-toc-text"> <span class="vector-toc-numb">7</span> <span>External links</span> </div> </a> <ul id="toc-External_links-sublist" class="vector-toc-list"> </ul> </li> </ul> </div> </div> </nav> </div> </div> <div class="mw-content-container"> <main id="content" class="mw-body"> <header class="mw-body-header vector-page-titlebar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-page-titlebar-toc" class="vector-dropdown vector-page-titlebar-toc vector-button-flush-left" > <input type="checkbox" id="vector-page-titlebar-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-titlebar-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-page-titlebar-toc-label" for="vector-page-titlebar-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-titlebar-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">Lean (proof assistant)</span></h1> <div id="p-lang-btn" class="vector-dropdown mw-portlet mw-portlet-lang" > <input type="checkbox" id="p-lang-btn-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-lang-btn" class="vector-dropdown-checkbox mw-interlanguage-selector" aria-label="Go to an article in another language. Available in 12 languages" > <label id="p-lang-btn-label" for="p-lang-btn-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive mw-portlet-lang-heading-12" aria-hidden="true" ><span class="vector-icon mw-ui-icon-language-progressive mw-ui-icon-wikimedia-language-progressive"></span> <span class="vector-dropdown-label-text">12 languages</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="interlanguage-link interwiki-cs mw-list-item"><a href="https://cs.wikipedia.org/wiki/Lean_(programovac%C3%AD_jazyk)" title="Lean (programovací jazyk) – Czech" lang="cs" hreflang="cs" data-title="Lean (programovací jazyk)" data-language-autonym="Čeština" data-language-local-name="Czech" class="interlanguage-link-target"><span>Čeština</span></a></li><li class="interlanguage-link interwiki-de mw-list-item"><a href="https://de.wikipedia.org/wiki/Lean_(Beweisassistent)" title="Lean (Beweisassistent) – German" lang="de" hreflang="de" data-title="Lean (Beweisassistent)" data-language-autonym="Deutsch" data-language-local-name="German" class="interlanguage-link-target"><span>Deutsch</span></a></li><li class="interlanguage-link interwiki-es mw-list-item"><a href="https://es.wikipedia.org/wiki/Lean" title="Lean – Spanish" lang="es" hreflang="es" data-title="Lean" data-language-autonym="Español" data-language-local-name="Spanish" class="interlanguage-link-target"><span>Español</span></a></li><li class="interlanguage-link interwiki-fa mw-list-item"><a href="https://fa.wikipedia.org/wiki/%D9%84%DB%8C%D9%86_(%D8%AF%D8%B3%D8%AA%DB%8C%D8%A7%D8%B1_%D8%A7%D8%AB%D8%A8%D8%A7%D8%AA)" title="لین (دستیار اثبات) – Persian" lang="fa" hreflang="fa" data-title="لین (دستیار اثبات)" data-language-autonym="فارسی" data-language-local-name="Persian" class="interlanguage-link-target"><span>فارسی</span></a></li><li class="interlanguage-link interwiki-fr mw-list-item"><a href="https://fr.wikipedia.org/wiki/Lean_(assistant_de_preuve)" title="Lean (assistant de preuve) – French" lang="fr" hreflang="fr" data-title="Lean (assistant de preuve)" data-language-autonym="Français" data-language-local-name="French" class="interlanguage-link-target"><span>Français</span></a></li><li class="interlanguage-link interwiki-nl mw-list-item"><a href="https://nl.wikipedia.org/wiki/Lean_(bewijsassistent)" title="Lean (bewijsassistent) – Dutch" lang="nl" hreflang="nl" data-title="Lean (bewijsassistent)" data-language-autonym="Nederlands" data-language-local-name="Dutch" class="interlanguage-link-target"><span>Nederlands</span></a></li><li class="interlanguage-link interwiki-ja mw-list-item"><a href="https://ja.wikipedia.org/wiki/Lean_(%E8%A8%BC%E6%98%8E%E3%82%A2%E3%82%B7%E3%82%B9%E3%82%BF%E3%83%B3%E3%83%88)" title="Lean (証明アシスタント) – Japanese" lang="ja" hreflang="ja" data-title="Lean (証明アシスタント)" data-language-autonym="日本語" data-language-local-name="Japanese" class="interlanguage-link-target"><span>日本語</span></a></li><li class="interlanguage-link interwiki-pt mw-list-item"><a href="https://pt.wikipedia.org/wiki/Lean_(linguagem_de_programa%C3%A7%C3%A3o)" title="Lean (linguagem de programação) – Portuguese" lang="pt" hreflang="pt" data-title="Lean (linguagem de programação)" data-language-autonym="Português" data-language-local-name="Portuguese" class="interlanguage-link-target"><span>Português</span></a></li><li class="interlanguage-link interwiki-ru mw-list-item"><a href="https://ru.wikipedia.org/wiki/Lean" title="Lean – Russian" lang="ru" hreflang="ru" data-title="Lean" data-language-autonym="Русский" data-language-local-name="Russian" class="interlanguage-link-target"><span>Русский</span></a></li><li class="interlanguage-link interwiki-uk mw-list-item"><a href="https://uk.wikipedia.org/wiki/Lean" title="Lean – Ukrainian" lang="uk" hreflang="uk" data-title="Lean" data-language-autonym="Українська" data-language-local-name="Ukrainian" class="interlanguage-link-target"><span>Українська</span></a></li><li class="interlanguage-link interwiki-vi mw-list-item"><a href="https://vi.wikipedia.org/wiki/Lean_(tr%E1%BB%A3_l%C3%BD_ch%E1%BB%A9ng_minh)" title="Lean (trợ lý chứng minh) – Vietnamese" lang="vi" hreflang="vi" data-title="Lean (trợ lý chứng minh)" data-language-autonym="Tiếng Việt" data-language-local-name="Vietnamese" class="interlanguage-link-target"><span>Tiếng Việt</span></a></li><li class="interlanguage-link interwiki-zh mw-list-item"><a href="https://zh.wikipedia.org/wiki/Lean" title="Lean – Chinese" lang="zh" hreflang="zh" data-title="Lean" data-language-autonym="中文" data-language-local-name="Chinese" class="interlanguage-link-target"><span>中文</span></a></li> </ul> <div class="after-portlet after-portlet-lang"><span class="wb-langlinks-edit wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q6509476#sitelinks-wikipedia" title="Edit interlanguage links" class="wbc-editpage">Edit links</a></span></div> </div> </div> </div> </header> <div class="vector-page-toolbar"> <div class="vector-page-toolbar-container"> <div id="left-navigation"> <nav aria-label="Namespaces"> <div id="p-associated-pages" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-associated-pages" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Lean_(proof_assistant)" title="View the content page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Talk:Lean_(proof_assistant)" rel="discussion" title="Discuss improvements to the content page [t]" accesskey="t"><span>Talk</span></a></li> </ul> </div> </div> <div id="vector-variants-dropdown" class="vector-dropdown emptyPortlet" > <input type="checkbox" id="vector-variants-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-variants-dropdown" class="vector-dropdown-checkbox " aria-label="Change language variant" > <label id="vector-variants-dropdown-label" for="vector-variants-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">English</span> </label> <div class="vector-dropdown-content"> <div id="p-variants" class="vector-menu mw-portlet mw-portlet-variants emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> </div> </div> </nav> </div> <div id="right-navigation" class="vector-collapsible"> <nav aria-label="Views"> <div id="p-views" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-views" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Lean_(proof_assistant)"><span>Read</span></a></li><li id="ca-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Lean_(proof_assistant)&action=history" title="Past revisions of this page [h]" accesskey="h"><span>View history</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-dropdown" class="vector-dropdown vector-page-tools-dropdown" > <input type="checkbox" id="vector-page-tools-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-tools-dropdown" class="vector-dropdown-checkbox " aria-label="Tools" > <label id="vector-page-tools-dropdown-label" for="vector-page-tools-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">Tools</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-tools-unpinned-container" class="vector-unpinned-container"> <div id="vector-page-tools" class="vector-page-tools vector-pinnable-element"> <div class="vector-pinnable-header vector-page-tools-pinnable-header vector-pinnable-header-unpinned" data-feature-name="page-tools-pinned" data-pinnable-element-id="vector-page-tools" data-pinned-container-id="vector-page-tools-pinned-container" data-unpinned-container-id="vector-page-tools-unpinned-container" > <div class="vector-pinnable-header-label">Tools</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">hide</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="More options" > <div class="vector-menu-heading"> Actions </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-more-view" class="selected vector-more-collapsible-item mw-list-item"><a href="/wiki/Lean_(proof_assistant)"><span>Read</span></a></li><li id="ca-more-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Lean_(proof_assistant)&action=history"><span>View history</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> General </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Special:WhatLinksHere/Lean_(proof_assistant)" title="List of all English Wikipedia pages containing links to this page [j]" accesskey="j"><span>What links here</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Special:RecentChangesLinked/Lean_(proof_assistant)" rel="nofollow" title="Recent changes in pages linked from this page [k]" accesskey="k"><span>Related changes</span></a></li><li id="t-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_Upload_Wizard" title="Upload files [u]" accesskey="u"><span>Upload file</span></a></li><li id="t-specialpages" class="mw-list-item"><a href="/wiki/Special:SpecialPages" title="A list of all special pages [q]" accesskey="q"><span>Special pages</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=Lean_(proof_assistant)&oldid=1254178588" title="Permanent link to this revision of this page"><span>Permanent link</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=Lean_(proof_assistant)&action=info" title="More information about this page"><span>Page information</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Special:CiteThisPage&page=Lean_%28proof_assistant%29&id=1254178588&wpFormIdentifier=titleform" title="Information on how to cite this page"><span>Cite this page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Special:UrlShortener&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FLean_%28proof_assistant%29"><span>Get shortened URL</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Special:QrCode&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FLean_%28proof_assistant%29"><span>Download QR code</span></a></li> </ul> </div> </div> <div id="p-coll-print_export" class="vector-menu mw-portlet mw-portlet-coll-print_export" > <div class="vector-menu-heading"> Print/export </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Special:DownloadAsPdf&page=Lean_%28proof_assistant%29&action=show-download-screen" title="Download this page as a PDF file"><span>Download as PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=Lean_(proof_assistant)&printable=yes" title="Printable version of this page [p]" accesskey="p"><span>Printable version</span></a></li> </ul> </div> </div> <div id="p-wikibase-otherprojects" class="vector-menu mw-portlet mw-portlet-wikibase-otherprojects" > <div class="vector-menu-heading"> In other projects </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q6509476" title="Structured data on this page hosted by Wikidata [g]" accesskey="g"><span>Wikidata item</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> </div> </div> </div> <div class="vector-column-end"> <div class="vector-sticky-pinned-container"> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-pinned-container" class="vector-pinned-container"> <div id="vector-appearance" class="vector-appearance vector-pinnable-element"> <div class="vector-pinnable-header vector-appearance-pinnable-header vector-pinnable-header-pinned" data-feature-name="appearance-pinned" data-pinnable-element-id="vector-appearance" data-pinned-container-id="vector-appearance-pinned-container" data-unpinned-container-id="vector-appearance-unpinned-container" > <div class="vector-pinnable-header-label">Appearance</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">hide</button> </div> </div> </div> </nav> </div> </div> <div id="bodyContent" class="vector-body" aria-labelledby="firstHeading" data-mw-ve-target-container> <div class="vector-body-before-content"> <div class="mw-indicators"> </div> <div id="siteSub" class="noprint">From Wikipedia, the free encyclopedia</div> </div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><div class="shortdescription nomobile noexcerpt noprint searchaux" style="display:none">Proof assistant and programming language</div> <style data-mw-deduplicate="TemplateStyles:r1257001546">.mw-parser-output .infobox-subbox{padding:0;border:none;margin:-3px;width:auto;min-width:100%;font-size:100%;clear:none;float:none;background-color:transparent}.mw-parser-output .infobox-3cols-child{margin:auto}.mw-parser-output .infobox .navbar{font-size:100%}@media screen{html.skin-theme-clientpref-night .mw-parser-output .infobox-full-data:not(.notheme)>div:not(.notheme)[style]{background:#1f1f23!important;color:#f8f9fa}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .infobox-full-data:not(.notheme) div:not(.notheme){background:#1f1f23!important;color:#f8f9fa}}@media(min-width:640px){body.skin--responsive .mw-parser-output .infobox-table{display:table!important}body.skin--responsive .mw-parser-output .infobox-table>caption{display:table-caption!important}body.skin--responsive .mw-parser-output .infobox-table>tbody{display:table-row-group}body.skin--responsive .mw-parser-output .infobox-table tr{display:table-row!important}body.skin--responsive .mw-parser-output .infobox-table th,body.skin--responsive .mw-parser-output .infobox-table td{padding-left:inherit;padding-right:inherit}}</style><table class="infobox vevent"><caption class="infobox-title summary">Lean</caption><tbody><tr><td colspan="2" class="infobox-image"><span typeof="mw:File"><a href="/wiki/File:Lean_logo2.svg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/d/dc/Lean_logo2.svg/220px-Lean_logo2.svg.png" decoding="async" width="220" height="69" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/d/dc/Lean_logo2.svg/330px-Lean_logo2.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/d/dc/Lean_logo2.svg/440px-Lean_logo2.svg.png 2x" data-file-width="963" data-file-height="300" /></a></span></td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Programming_paradigm" title="Programming paradigm">Paradigm</a></th><td class="infobox-data"><a href="/wiki/Functional_programming" title="Functional programming">Functional programming</a>, <a href="/wiki/Imperative_programming" title="Imperative programming">Imperative programming</a></td></tr><tr><th scope="row" class="infobox-label">Family</th><td class="infobox-data"><a href="/wiki/Proof_assistant" title="Proof assistant">Proof assistant</a></td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Software_developer" class="mw-redirect" title="Software developer">Developer</a></th><td class="infobox-data organiser"><a rel="nofollow" class="external text" href="https://lean-fro.org/">Lean FRO</a></td></tr><tr><th scope="row" class="infobox-label">First appeared</th><td class="infobox-data">2013<span class="noprint">; 11 years ago</span><span style="display:none"> (<span class="bday dtstart published updated">2013</span>)</span></td></tr><tr><td colspan="2" class="infobox-full-data"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1257001546"></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Software_release_life_cycle" title="Software release life cycle">Stable release</a></th><td class="infobox-data"><div style="margin:0px;"><a rel="nofollow" class="external text" href="https://github.com/leanprover/lean4/releases/latest">4.11.0</a> / 1 September 2024<span class="noprint">; 2 months ago</span><span style="display:none"> (<span class="bday dtstart published updated">2024-09-01</span>)</span></div></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Software_release_life_cycle#Beta" title="Software release life cycle">Preview release</a></th><td class="infobox-data"><div style="margin:0px;"><a rel="nofollow" class="external text" href="https://github.com/leanprover/lean4/releases/tag/v4.12.0-rc1">4.12.0-rc1</a> / 2 September 2024<span class="noprint">; 2 months ago</span><span style="display:none"> (<span class="bday dtstart published updated">2024-09-02</span>)</span></div></td></tr><tr style="display:none"><td colspan="2"> </td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Type_system" title="Type system">Typing discipline</a></th><td class="infobox-data"><a href="/wiki/Static_typing" class="mw-redirect" title="Static typing">Static</a>, <a href="/wiki/Strong_and_weak_typing" title="Strong and weak typing">strong</a>, <a href="/wiki/Type_inference" title="Type inference">inferred</a></td></tr><tr><th scope="row" class="infobox-label">Implementation language</th><td class="infobox-data">Lean, <a href="/wiki/C%2B%2B" title="C++">C++</a></td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Operating_system" title="Operating system">OS</a></th><td class="infobox-data"><a href="/wiki/Cross-platform" class="mw-redirect" title="Cross-platform">Cross-platform</a></td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Software_license" title="Software license">License</a></th><td class="infobox-data"><a href="/wiki/Apache_License_2.0" class="mw-redirect" title="Apache License 2.0">Apache License 2.0</a></td></tr><tr><th scope="row" class="infobox-label">Website</th><td class="infobox-data"><span class="url"><a rel="nofollow" class="external text" href="https://lean-lang.org/">lean-lang<wbr />.org</a></span></td></tr><tr><th colspan="2" class="infobox-header" style="background-color: #eee;">Influenced by</th></tr><tr><td colspan="2" class="infobox-full-data"><a href="/wiki/ML_(programming_language)" title="ML (programming language)">ML</a><br /><a href="/wiki/Coq_(software)" title="Coq (software)">Coq</a><br /><a href="/wiki/Haskell" title="Haskell">Haskell</a></td></tr></tbody></table> <p><b>Lean</b> is a <a href="/wiki/Proof_assistant" title="Proof assistant">proof assistant</a> and a <a href="/wiki/Functional_programming" title="Functional programming">functional programming language</a>.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> It is based on the <a href="/wiki/Calculus_of_constructions" title="Calculus of constructions">calculus of constructions</a> with <a href="/wiki/Inductive_type" title="Inductive type">inductive types</a>. It is an <a href="/wiki/Open-source" class="mw-redirect" title="Open-source">open-source</a> project hosted on <a href="/wiki/GitHub" title="GitHub">GitHub</a>. It was developed primarily by <a href="/w/index.php?title=Leonardo_de_Moura&action=edit&redlink=1" class="new" title="Leonardo de Moura (page does not exist)">Leonardo de Moura</a> while employed by <a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research</a> and now <a href="/wiki/Amazon_Web_Services" title="Amazon Web Services">Amazon Web Services</a>, and has had significant contributions from other coauthors and collaborators during its history. Development is currently supported by the <a href="/wiki/Nonprofit_organization" title="Nonprofit organization">non-profit</a> Lean <a href="/wiki/Focused_Research_Organization" class="mw-redirect" title="Focused Research Organization">Focused Research Organization (FRO)</a>. </p> <meta property="mw:PageProp/toc" /> <div class="mw-heading mw-heading2"><h2 id="History">History</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=1" title="Edit section: History"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Lean was launched by Leonardo de Moura at <a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research</a> in 2013.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> The initial versions of the language, later known as Lean 1 and 2, were experimental and contained features such as support for <a href="/wiki/Homotopy_type_theory" title="Homotopy type theory">homotopy type theory</a> – based foundations that were later dropped. </p><p>Lean 3 (first released Jan 20, 2017) was the first moderately stable version of Lean. It was implemented primarily in C++ with some features written in Lean itself. After version 3.4.2 Lean 3 was officially end-of-lifed while development of Lean 4 began. In this interim period members of the Lean community developed and released unofficial versions up to 3.51.1. </p><p>In 2021, Lean 4 was released, which was a reimplementation of the Lean theorem prover capable of producing <a href="/wiki/C_(programming_language)" title="C (programming language)">C</a> code which is then compiled, enabling the development of efficient domain-specific automation.<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> Lean 4 also contains a macro system and improved <a href="/wiki/Type_class" title="Type class">type class</a> synthesis and memory management procedures over the previous version. Another benefit compared to Lean 3 is the ability to avoid touching C++ code in order to modify the frontend and other key parts of the core system, as they are now all implemented in Lean and available to the end user to be overridden as needed.<sup class="noprint Inline-Template Template-Fact" style="white-space:nowrap;">[<i><a href="/wiki/Wikipedia:Citation_needed" title="Wikipedia:Citation needed"><span title="This claim needs references to reliable sources. (October 2023)">citation needed</span></a></i>]</sup> </p><p>Lean 4 is not <a href="/wiki/Backward_compatibility" title="Backward compatibility">backwards-compatible</a> with Lean 3.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup> </p><p>In 2023, the Lean FRO was formed, with the goals of improving the language's scalability and usability, and implementing <a href="/wiki/Proof_automation" class="mw-redirect" title="Proof automation">proof automation</a>.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading2"><h2 id="Overview">Overview</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=2" title="Edit section: Overview"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading3"><h3 id="Libraries">Libraries</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=3" title="Edit section: Libraries"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The official lean package includes a <a href="/wiki/Standard_library" title="Standard library">standard library</a> <i>batteries</i>, which implements common <a href="/wiki/Data_structure" title="Data structure">data structures</a> that may be used for both mathematical research and more conventional software development.<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> </p><p>In 2017, a community-maintained project to develop a Lean library <i>mathlib</i> began, with the goal to digitize as much of <a href="/wiki/Pure_mathematics" title="Pure mathematics">pure mathematics</a> as possible in one large cohesive library, up to research level mathematics.<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup> As of September 2024, mathlib had formalised over 165,000 theorems and 85,000 definitions in Lean.<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading3"><h3 id="Editors_integration">Editors integration</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=4" title="Edit section: Editors integration"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Lean integrates with:<sup id="cite_ref-10" class="reference"><a href="#cite_note-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup> </p> <ul><li><a href="/wiki/Visual_Studio_Code" title="Visual Studio Code">Visual Studio Code</a></li> <li><a href="/wiki/Neovim" class="mw-redirect" title="Neovim">Neovim</a></li> <li><a href="/wiki/Emacs" title="Emacs">Emacs</a></li></ul> <p>Interfacing is done via a client-extension and <a href="/wiki/Language_Server_Protocol" title="Language Server Protocol">Language Server Protocol</a> server. </p><p>It has native support for <a href="/wiki/Unicode" title="Unicode">Unicode</a> symbols, which can be typed using <a href="/wiki/LaTeX" title="LaTeX">LaTeX</a>-like sequences, such as "\times" for "×". Lean can also be compiled to <a href="/wiki/JavaScript" title="JavaScript">JavaScript</a> and accessed in a web browser and has extensive support for <a href="/wiki/Meta-programming" class="mw-redirect" title="Meta-programming">meta-programming</a>. </p> <div class="mw-heading mw-heading2"><h2 id="Examples_(Lean_4)"><span id="Examples_.28Lean_4.29"></span>Examples (Lean 4)</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=5" title="Edit section: Examples (Lean 4)"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The <a href="/wiki/Natural_numbers" class="mw-redirect" title="Natural numbers">natural numbers</a> can be defined as an <a href="/wiki/Inductive_type" title="Inductive type">inductive type</a>. This definition is based on the <a href="/wiki/Peano_axioms" title="Peano axioms">Peano axioms</a> and states that every natural number is either zero or the <a href="/wiki/Successor_function" title="Successor function">successor</a> of some other natural number. </p> <div class="mw-highlight mw-highlight-lang-lean mw-content-ltr" dir="ltr"><pre><span></span><span class="kd">inductive</span> <span class="n">Nat</span> <span class="o">:</span> <span class="kt">Type</span> <span class="bp">|</span> <span class="n">zero</span> <span class="o">:</span> <span class="n">Nat</span> <span class="bp">|</span> <span class="n">succ</span> <span class="o">:</span> <span class="n">Nat</span> <span class="bp">→</span> <span class="n">Nat</span> </pre></div> <p>Addition of natural numbers can be <a href="/wiki/Recursive_definition" title="Recursive definition">defined recursively</a>, using <a href="/wiki/Pattern_matching" title="Pattern matching">pattern matching</a>. </p> <div class="mw-highlight mw-highlight-lang-lean mw-content-ltr" dir="ltr"><pre><span></span><span class="kd">def</span> <span class="n">Nat.add</span> <span class="o">:</span> <span class="n">Nat</span> <span class="bp">→</span> <span class="n">Nat</span> <span class="bp">→</span> <span class="n">Nat</span> <span class="bp">|</span> <span class="n">n</span><span class="o">,</span> <span class="n">Nat.zero</span> <span class="bp">=></span> <span class="n">n</span> <span class="c1">-- n + 0 = n </span> <span class="bp">|</span> <span class="n">n</span><span class="o">,</span> <span class="n">Nat.succ</span> <span class="n">m</span> <span class="bp">=></span> <span class="n">Nat.succ</span> <span class="o">(</span><span class="n">Nat.add</span> <span class="n">n</span> <span class="n">m</span><span class="o">)</span> <span class="c1">-- n + succ(m) = succ(n + m)</span> </pre></div> <p>This is a simple proof of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (P\wedge Q)\implies (Q\wedge P)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>P</mi> <mo>∧</mo> <mi>Q</mi> <mo stretchy="false">)</mo> <mspace width="thickmathspace" /> <mo stretchy="false">⟹</mo> <mspace width="thickmathspace" /> <mo stretchy="false">(</mo> <mi>Q</mi> <mo>∧</mo> <mi>P</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (P\wedge Q)\implies (Q\wedge P)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9a37706803da2da2a232617eb8ba4da537445a5e" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:22.338ex; height:2.843ex;" alt="{\displaystyle (P\wedge Q)\implies (Q\wedge P)}"></span> for two <a href="/wiki/Proposition" title="Proposition">propositions</a> <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>P</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle P}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b4dc73bf40314945ff376bd363916a738548d40a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>Q</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle Q}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8752c7023b4b3286800fe3238271bbca681219ed" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}"></span> (where <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \wedge }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>∧</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \wedge }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1caa4004cb216ef2930bb12fe805a76870caed94" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \wedge }"></span> is the <a href="/wiki/Logical_conjunction" title="Logical conjunction">conjunction</a> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \implies }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mspace width="thickmathspace" /> <mo stretchy="false">⟹</mo> <mspace width="thickmathspace" /> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \implies }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/913c2e89ea94dfa446f69b056d4bf505e01fcc5f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.096ex; height:1.843ex;" alt="{\displaystyle \implies }"></span> the <a href="/wiki/Material_conditional" title="Material conditional">implication</a>) in Lean using tactic mode: </p> <div class="mw-highlight mw-highlight-lang-lean mw-content-ltr" dir="ltr"><pre><span></span><span class="kd">theorem</span> <span class="n">and_swap</span> <span class="o">(</span><span class="n">p</span> <span class="n">q</span> <span class="o">:</span> <span class="kt">Prop</span><span class="o">)</span> <span class="o">:</span> <span class="n">p</span> <span class="bp">∧</span> <span class="n">q</span> <span class="bp">→</span> <span class="n">q</span> <span class="bp">∧</span> <span class="n">p</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">intro</span> <span class="n">h</span> <span class="c1">-- assume p ∧ q with proof h, the goal is q ∧ p</span> <span class="n">apply</span> <span class="n">And.intro</span> <span class="c1">-- the goal is split into two subgoals, one is q and the other is p</span> <span class="bp">·</span> <span class="n">exact</span> <span class="n">h.right</span> <span class="c1">-- the first subgoal is exactly the right part of h : p ∧ q</span> <span class="bp">·</span> <span class="n">exact</span> <span class="n">h.left</span> <span class="c1">-- the second subgoal is exactly the left part of h : p ∧ q</span> </pre></div> <p>This same proof in term mode: </p> <div class="mw-highlight mw-highlight-lang-lean mw-content-ltr" dir="ltr"><pre><span></span><span class="kd">theorem</span> <span class="n">and_swap</span> <span class="o">(</span><span class="n">p</span> <span class="n">q</span> <span class="o">:</span> <span class="kt">Prop</span><span class="o">)</span> <span class="o">:</span> <span class="n">p</span> <span class="bp">∧</span> <span class="n">q</span> <span class="bp">→</span> <span class="n">q</span> <span class="bp">∧</span> <span class="n">p</span> <span class="o">:=</span> <span class="k">fun</span> <span class="o">⟨</span><span class="n">hp</span><span class="o">,</span> <span class="n">hq</span><span class="o">⟩</span> <span class="bp">=></span> <span class="o">⟨</span><span class="n">hq</span><span class="o">,</span> <span class="n">hp</span><span class="o">⟩</span> </pre></div> <div class="mw-heading mw-heading2"><h2 id="Usage">Usage</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=6" title="Edit section: Usage"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading3"><h3 id="Mathematics">Mathematics</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=7" title="Edit section: Mathematics"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1236090951">.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}</style><div role="note" class="hatnote navigation-not-searchable">See also: <a href="/wiki/Proof_assistant#Notable_formalized_proofs" title="Proof assistant">Proof assistant § Notable formalized proofs</a></div> <p>Lean has received attention from mathematicians such as <a href="/wiki/Thomas_Callister_Hales" title="Thomas Callister Hales">Thomas Hales</a>,<sup id="cite_ref-11" class="reference"><a href="#cite_note-11"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup> <a href="/wiki/Kevin_Buzzard" title="Kevin Buzzard">Kevin Buzzard</a>,<sup id="cite_ref-Buzzard_12-0" class="reference"><a href="#cite_note-Buzzard-12"><span class="cite-bracket">[</span>12<span class="cite-bracket">]</span></a></sup> and Heather Macbeth.<sup id="cite_ref-13" class="reference"><a href="#cite_note-13"><span class="cite-bracket">[</span>13<span class="cite-bracket">]</span></a></sup> Hales is using it for his project, Formal Abstracts.<sup id="cite_ref-14" class="reference"><a href="#cite_note-14"><span class="cite-bracket">[</span>14<span class="cite-bracket">]</span></a></sup> Buzzard uses it for the Xena project.<sup id="cite_ref-15" class="reference"><a href="#cite_note-15"><span class="cite-bracket">[</span>15<span class="cite-bracket">]</span></a></sup> One of the Xena Project's goals is to rewrite every theorem and proof in the undergraduate math curriculum of <a href="/wiki/Imperial_College_London" title="Imperial College London">Imperial College London</a> in Lean. Macbeth is using Lean to teach students the fundamentals of mathematical proof with instant feedback.<sup id="cite_ref-16" class="reference"><a href="#cite_note-16"><span class="cite-bracket">[</span>16<span class="cite-bracket">]</span></a></sup> </p><p>In 2021, a team of researchers used Lean to verify the correctness of a proof by <a href="/wiki/Peter_Scholze" title="Peter Scholze">Peter Scholze</a> in the area of <a href="/wiki/Condensed_mathematics" title="Condensed mathematics">condensed mathematics</a>. The project garnered attention for formalizing a result at the cutting edge of mathematical research.<sup id="cite_ref-Quanta21_17-0" class="reference"><a href="#cite_note-Quanta21-17"><span class="cite-bracket">[</span>17<span class="cite-bracket">]</span></a></sup> In 2023, <a href="/wiki/Terence_Tao" title="Terence Tao">Terence Tao</a> used Lean to formalize a proof of the <a href="/wiki/Freiman%27s_theorem" title="Freiman's theorem">Polynomial Freiman-Ruzsa</a> (PFR) conjecture, a result published by Tao and collaborators in the same year.<sup id="cite_ref-18" class="reference"><a href="#cite_note-18"><span class="cite-bracket">[</span>18<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading3"><h3 id="Artificial_intelligence">Artificial intelligence</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=8" title="Edit section: Artificial intelligence"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>In 2022, <a href="/wiki/OpenAI" title="OpenAI">OpenAI</a> and <a href="/wiki/Meta_AI" title="Meta AI">Meta AI</a> independently created AI models to generate proofs of various high-school-level olympiad problems in Lean.<sup id="cite_ref-19" class="reference"><a href="#cite_note-19"><span class="cite-bracket">[</span>19<span class="cite-bracket">]</span></a></sup> Meta AI's model is available for public use with the Lean environment.<sup id="cite_ref-20" class="reference"><a href="#cite_note-20"><span class="cite-bracket">[</span>20<span class="cite-bracket">]</span></a></sup> </p><p>In 2023, <a href="/wiki/Vlad_Tenev" title="Vlad Tenev">Vlad Tenev</a> and Tudor Achim co-founded startup Harmonic, which aims to reduce <a href="/wiki/Hallucination_(artificial_intelligence)" title="Hallucination (artificial intelligence)">AI hallucinations</a> by generating and checking Lean code.<sup id="cite_ref-21" class="reference"><a href="#cite_note-21"><span class="cite-bracket">[</span>21<span class="cite-bracket">]</span></a></sup> </p><p>In 2024, <a href="/wiki/Google_DeepMind" title="Google DeepMind">Google DeepMind</a> created <a href="/wiki/Google_DeepMind#AlphaProof" title="Google DeepMind">AlphaProof</a><sup id="cite_ref-22" class="reference"><a href="#cite_note-22"><span class="cite-bracket">[</span>22<span class="cite-bracket">]</span></a></sup> which proves mathematical statements in Lean at the level of a silver medalist at the <a href="/wiki/International_Mathematical_Olympiad" title="International Mathematical Olympiad">International Mathematical Olympiad</a>. This was the first AI system that achieved a medal-worthy performance on a math olympiad's problems.<sup id="cite_ref-23" class="reference"><a href="#cite_note-23"><span class="cite-bracket">[</span>23<span class="cite-bracket">]</span></a></sup> </p><p><br /> </p> <div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=9" title="Edit section: See also"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1239009302">.mw-parser-output .portalbox{padding:0;margin:0.5em 0;display:table;box-sizing:border-box;max-width:175px;list-style:none}.mw-parser-output .portalborder{border:1px solid var(--border-color-base,#a2a9b1);padding:0.1em;background:var(--background-color-neutral-subtle,#f8f9fa)}.mw-parser-output .portalbox-entry{display:table-row;font-size:85%;line-height:110%;height:1.9em;font-style:italic;font-weight:bold}.mw-parser-output .portalbox-image{display:table-cell;padding:0.2em;vertical-align:middle;text-align:center}.mw-parser-output .portalbox-link{display:table-cell;padding:0.2em 0.2em 0.2em 0.3em;vertical-align:middle}@media(min-width:720px){.mw-parser-output .portalleft{clear:left;float:left;margin:0.5em 1em 0.5em 0}.mw-parser-output .portalright{clear:right;float:right;margin:0.5em 0 0.5em 1em}}</style><ul role="navigation" aria-label="Portals" class="noprint portalbox portalborder portalright"> <li class="portalbox-entry"><span class="portalbox-image"><span class="noviewer" typeof="mw:File"><a href="/wiki/File:Nuvola_apps_edu_mathematics_blue-p.svg" class="mw-file-description"><img alt="icon" src="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/28px-Nuvola_apps_edu_mathematics_blue-p.svg.png" decoding="async" width="28" height="28" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/42px-Nuvola_apps_edu_mathematics_blue-p.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/56px-Nuvola_apps_edu_mathematics_blue-p.svg.png 2x" data-file-width="128" data-file-height="128" /></a></span></span><span class="portalbox-link"><a href="/wiki/Portal:Mathematics" title="Portal:Mathematics">Mathematics portal</a></span></li><li class="portalbox-entry"><span class="portalbox-image"><span class="noviewer" typeof="mw:File"><span><img alt="" src="//upload.wikimedia.org/wikipedia/commons/thumb/3/31/Free_and_open-source_software_logo_%282009%29.svg/28px-Free_and_open-source_software_logo_%282009%29.svg.png" decoding="async" width="28" height="28" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/3/31/Free_and_open-source_software_logo_%282009%29.svg/42px-Free_and_open-source_software_logo_%282009%29.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/3/31/Free_and_open-source_software_logo_%282009%29.svg/56px-Free_and_open-source_software_logo_%282009%29.svg.png 2x" data-file-width="512" data-file-height="512" /></span></span></span><span class="portalbox-link"><a href="/wiki/Portal:Free_and_open-source_software" title="Portal:Free and open-source software">Free and open-source software portal</a></span></li></ul> <ul><li><a href="/wiki/Dependent_type" title="Dependent type">Dependent type</a></li> <li><a href="/wiki/List_of_proof_assistants" class="mw-redirect" title="List of proof assistants">List of proof assistants</a></li> <li><a href="/wiki/Mimalloc" title="Mimalloc">mimalloc</a></li> <li><a href="/wiki/Type_theory" title="Type theory">Type theory</a></li></ul> <div class="mw-heading mw-heading2"><h2 id="References">References</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=10" title="Edit section: References"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1239543626">.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}</style><div class="reflist"> <div class="mw-references-wrap mw-references-columns"><ol class="references"> <li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text"><style data-mw-deduplicate="TemplateStyles:r1238218222">.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}</style><cite id="CITEREFMouraUllrich2021" class="citation journal cs1">Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, André; Sutcliffe, Geoff (eds.). <a rel="nofollow" class="external text" href="https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37">"The Lean 4 Theorem Prover and Programming Language"</a>. <i>Automated Deduction – CADE 28</i>. Cham: Springer International Publishing: 625–635. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-030-79876-5_37">10.1007/978-3-030-79876-5_37</a></span>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-3-030-79876-5" title="Special:BookSources/978-3-030-79876-5"><bdi>978-3-030-79876-5</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Automated+Deduction+%E2%80%93+CADE+28&rft.atitle=The+Lean+4+Theorem+Prover+and+Programming+Language&rft.pages=625-635&rft.date=2021&rft_id=info%3Adoi%2F10.1007%2F978-3-030-79876-5_37&rft.isbn=978-3-030-79876-5&rft.aulast=Moura&rft.aufirst=Leonardo+de&rft.au=Ullrich%2C+Sebastian&rft_id=https%3A%2F%2Flink.springer.com%2Fchapter%2F10.1007%2F978-3-030-79876-5_37&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://lean-lang.org/about/">"About"</a>. <i>Lean Language</i><span class="reference-accessdate">. Retrieved <span class="nowrap">2024-03-13</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Lean+Language&rft.atitle=About&rft_id=https%3A%2F%2Flean-lang.org%2Fabout%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFMouraUllrich2021" class="citation book cs1">Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, Andr'e; Sutcliffe, Geoff (eds.). <a rel="nofollow" class="external text" href="https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37"><i>Automated Deduction -- CADE 28</i></a>. Springer International Publishing. pp. 625–635. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-030-79876-5_37">10.1007/978-3-030-79876-5_37</a>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-3-030-79876-5" title="Special:BookSources/978-3-030-79876-5"><bdi>978-3-030-79876-5</bdi></a>. <a href="/wiki/S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:235800962">235800962</a><span class="reference-accessdate">. Retrieved <span class="nowrap">24 March</span> 2023</span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Automated+Deduction+--+CADE+28&rft.pages=625-635&rft.pub=Springer+International+Publishing&rft.date=2021&rft_id=https%3A%2F%2Fapi.semanticscholar.org%2FCorpusID%3A235800962%23id-name%3DS2CID&rft_id=info%3Adoi%2F10.1007%2F978-3-030-79876-5_37&rft.isbn=978-3-030-79876-5&rft.aulast=Moura&rft.aufirst=Leonardo+de&rft.au=Ullrich%2C+Sebastian&rft_id=https%3A%2F%2Flink.springer.com%2Fchapter%2F10.1007%2F978-3-030-79876-5_37&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://leanprover.github.io/lean4/doc/lean3changes.html">"Significant changes from Lean 3"</a>. <i>Lean Manual</i><span class="reference-accessdate">. Retrieved <span class="nowrap">24 March</span> 2023</span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Lean+Manual&rft.atitle=Significant+changes+from+Lean+3&rft_id=https%3A%2F%2Fleanprover.github.io%2Flean4%2Fdoc%2Flean3changes.html&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://lean-fro.org/about/">"Mission"</a>. <i>Lean FRO</i>. 2023-07-25<span class="reference-accessdate">. Retrieved <span class="nowrap">2024-03-14</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Lean+FRO&rft.atitle=Mission&rft.date=2023-07-25&rft_id=https%3A%2F%2Flean-fro.org%2Fabout%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://github.com/leanprover-community/batteries">"batteries"</a>. <i><a href="/wiki/GitHub" title="GitHub">GitHub</a></i><span class="reference-accessdate">. Retrieved <span class="nowrap">2024-09-22</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=GitHub&rft.atitle=batteries&rft_id=https%3A%2F%2Fgithub.com%2Fleanprover-community%2Fbatteries&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://archive.today/20201002043743/https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/">"Building the Mathematical Library of the Future"</a>. <i><a href="/wiki/Quanta_Magazine" title="Quanta Magazine">Quanta Magazine</a></i>. Archived from <a rel="nofollow" class="external text" href="https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/">the original</a> on 2 Oct 2020.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Quanta+Magazine&rft.atitle=Building+the+Mathematical+Library+of+the+Future&rft_id=https%3A%2F%2Fwww.quantamagazine.org%2Fbuilding-the-mathematical-library-of-the-future-20201001%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://leanprover-community.github.io/lean3/">"Lean community"</a>. <i>leanprover-community.github.io</i><span class="reference-accessdate">. Retrieved <span class="nowrap">2023-10-24</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=leanprover-community.github.io&rft.atitle=Lean+community&rft_id=https%3A%2F%2Fleanprover-community.github.io%2Flean3%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://leanprover-community.github.io/mathlib_stats.html">"Mathlib statistics"</a>. <i>leanprover-community.github.io</i><span class="reference-accessdate">. Retrieved <span class="nowrap">2024-09-22</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=leanprover-community.github.io&rft.atitle=Mathlib+statistics&rft_id=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib_stats.html&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-10"><span class="mw-cite-backlink"><b><a href="#cite_ref-10">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://leanprover-community.github.io/install/linux.html">"Installing Lean 4 on Linux"</a>. <i>leanprover-community.github.io</i><span class="reference-accessdate">. Retrieved <span class="nowrap">2023-10-24</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=leanprover-community.github.io&rft.atitle=Installing+Lean+4+on+Linux&rft_id=https%3A%2F%2Fleanprover-community.github.io%2Finstall%2Flinux.html&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-11"><span class="mw-cite-backlink"><b><a href="#cite_ref-11">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFHales2018" class="citation web cs1">Hales, Thomas (September 18, 2018). <a rel="nofollow" class="external text" href="https://archive.today/20201121125544/https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/">"A Review of the Lean Theorem Prover"</a>. <i>Jigger Wit</i>. Archived from <a rel="nofollow" class="external text" href="https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/">the original</a> on 21 Nov 2020.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Jigger+Wit&rft.atitle=A+Review+of+the+Lean+Theorem+Prover&rft.date=2018-09-18&rft.aulast=Hales&rft.aufirst=Thomas&rft_id=https%3A%2F%2Fjiggerwit.wordpress.com%2F2018%2F09%2F18%2Fa-review-of-the-lean-theorem-prover%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-Buzzard-12"><span class="mw-cite-backlink"><b><a href="#cite_ref-Buzzard_12-0">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFBuzzard" class="citation web cs1">Buzzard, Kevin. <a rel="nofollow" class="external text" href="https://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf">"The Future of Mathematics?"</a> <span class="cs1-format">(PDF)</span><span class="reference-accessdate">. Retrieved <span class="nowrap">6 October</span> 2020</span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=unknown&rft.btitle=The+Future+of+Mathematics%3F&rft.aulast=Buzzard&rft.aufirst=Kevin&rft_id=https%3A%2F%2Fwwwf.imperial.ac.uk%2F~buzzard%2Fone_off_lectures%2Fmsr.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-13"><span class="mw-cite-backlink"><b><a href="#cite_ref-13">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFMacbeth" class="citation web cs1">Macbeth, Heather. <a rel="nofollow" class="external text" href="https://archive.today/20240605090236/https://hrmacbeth.github.io/math2001/">"The Mechanics of Proof"</a>. <i>hrmacbeth.github.io</i>. Archived from <a rel="nofollow" class="external text" href="https://hrmacbeth.github.io/math2001/">the original</a> on 5 Jun 2024.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=hrmacbeth.github.io&rft.atitle=The+Mechanics+of+Proof&rft.aulast=Macbeth&rft.aufirst=Heather&rft_id=https%3A%2F%2Fhrmacbeth.github.io%2Fmath2001%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-14"><span class="mw-cite-backlink"><b><a href="#cite_ref-14">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://formalabstracts.github.io/">"Formal Abstracts"</a>. <i>Github</i>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Github&rft.atitle=Formal+Abstracts&rft_id=https%3A%2F%2Fformalabstracts.github.io%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-15"><span class="mw-cite-backlink"><b><a href="#cite_ref-15">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://xenaproject.wordpress.com/what-is-the-xena-project/">"What is the Xena project?"</a>. <i>Xena</i>. 8 May 2019.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Xena&rft.atitle=What+is+the+Xena+project%3F&rft.date=2019-05-08&rft_id=https%3A%2F%2Fxenaproject.wordpress.com%2Fwhat-is-the-xena-project%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-16"><span class="mw-cite-backlink"><b><a href="#cite_ref-16">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFRoberts2023" class="citation web cs1">Roberts, Siobhan (July 2, 2023). <a rel="nofollow" class="external text" href="https://archive.today/20240501080422/https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html">"A.I. Is Coming for Mathematics, Too"</a>. <i>New York Times</i>. Archived from <a rel="nofollow" class="external text" href="https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html">the original</a> on 1 May 2024.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=New+York+Times&rft.atitle=A.I.+Is+Coming+for+Mathematics%2C+Too&rft.date=2023-07-02&rft.aulast=Roberts&rft.aufirst=Siobhan&rft_id=https%3A%2F%2Fwww.nytimes.com%2F2023%2F07%2F02%2Fscience%2Fai-mathematics-machine-learning.html&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-Quanta21-17"><span class="mw-cite-backlink"><b><a href="#cite_ref-Quanta21_17-0">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFHartnett2021" class="citation news cs1">Hartnett, Kevin (July 28, 2021). <a rel="nofollow" class="external text" href="https://archive.today/20220102145317/https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/">"Proof Assistant Makes Jump to Big-League Math"</a>. <i><a href="/wiki/Quanta_Magazine" title="Quanta Magazine">Quanta Magazine</a></i>. Archived from <a rel="nofollow" class="external text" href="https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/">the original</a> on 2 Jan 2022.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Quanta+Magazine&rft.atitle=Proof+Assistant+Makes+Jump+to+Big-League+Math&rft.date=2021-07-28&rft.aulast=Hartnett&rft.aufirst=Kevin&rft_id=https%3A%2F%2Fwww.quantamagazine.org%2Flean-computer-program-confirms-peter-scholze-proof-20210728%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-18"><span class="mw-cite-backlink"><b><a href="#cite_ref-18">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFSloman2023" class="citation web cs1">Sloman, Leila (2023-12-06). <a rel="nofollow" class="external text" href="https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/">"<span class="cs1-kern-left"></span>'A-Team' of Math Proves a Critical Link Between Addition and Sets"</a>. <i>Quanta Magazine</i><span class="reference-accessdate">. Retrieved <span class="nowrap">2023-12-07</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Quanta+Magazine&rft.atitle=%27A-Team%27+of+Math+Proves+a+Critical+Link+Between+Addition+and+Sets&rft.date=2023-12-06&rft.aulast=Sloman&rft.aufirst=Leila&rft_id=https%3A%2F%2Fwww.quantamagazine.org%2Fa-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-19"><span class="mw-cite-backlink"><b><a href="#cite_ref-19">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://openai.com/research/formal-math">"Solving (some) formal math olympiad problems"</a>. <i><a href="/wiki/OpenAI" title="OpenAI">OpenAI</a></i>. February 2, 2022<span class="reference-accessdate">. Retrieved <span class="nowrap">March 13,</span> 2024</span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=OpenAI&rft.atitle=Solving+%28some%29+formal+math+olympiad+problems&rft.date=2022-02-02&rft_id=https%3A%2F%2Fopenai.com%2Fresearch%2Fformal-math&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-20"><span class="mw-cite-backlink"><b><a href="#cite_ref-20">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://ai.meta.com/blog/ai-math-theorem-proving/">"Teaching AI advanced mathematical reasoning"</a>. <i><a href="/wiki/Meta_AI" title="Meta AI">Meta AI</a></i>. November 3, 2022<span class="reference-accessdate">. Retrieved <span class="nowrap">March 13,</span> 2024</span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Meta+AI&rft.atitle=Teaching+AI+advanced+mathematical+reasoning&rft.date=2022-11-03&rft_id=https%3A%2F%2Fai.meta.com%2Fblog%2Fai-math-theorem-proving%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-21"><span class="mw-cite-backlink"><b><a href="#cite_ref-21">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFMetz2024" class="citation news cs1">Metz, Cade (23 September 2024). <a rel="nofollow" class="external text" href="https://archive.today/20240924084639/https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html">"Is Math the Path to Chatbots That Don't Make Stuff Up?"</a>. <i>New York Times</i>. Archived from <a rel="nofollow" class="external text" href="https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html">the original</a> on 24 Sep 2024.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=New+York+Times&rft.atitle=Is+Math+the+Path+to+Chatbots+That+Don%E2%80%99t+Make+Stuff+Up%3F&rft.date=2024-09-23&rft.aulast=Metz&rft.aufirst=Cade&rft_id=https%3A%2F%2Fwww.nytimes.com%2F2024%2F09%2F23%2Ftechnology%2Fai-chatbots-chatgpt-math.html&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-22"><span class="mw-cite-backlink"><b><a href="#cite_ref-22">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/">"AI achieves silver-medal standard solving International Mathematical Olympiad problems"</a>. <i>Google DeepMind</i>. 2024-05-14<span class="reference-accessdate">. Retrieved <span class="nowrap">2024-07-25</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Google+DeepMind&rft.atitle=AI+achieves+silver-medal+standard+solving+International+Mathematical+Olympiad+problems&rft.date=2024-05-14&rft_id=https%3A%2F%2Fdeepmind.google%2Fdiscover%2Fblog%2Fai-solves-imo-problems-at-silver-medal-level%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> <li id="cite_note-23"><span class="mw-cite-backlink"><b><a href="#cite_ref-23">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFRoberts2024" class="citation web cs1">Roberts, Siobhan (July 25, 2024). <a rel="nofollow" class="external text" href="https://archive.today/20240729121148/https://www.nytimes.com/2024/07/25/science/ai-math-alphaproof-deepmind.html">"Move Over, Mathematicians, Here Comes AlphaProof"</a>. <i><a href="/wiki/New_York_Times" class="mw-redirect" title="New York Times">New York Times</a></i>. Archived from <a rel="nofollow" class="external text" href="https://www.nytimes.com/2024/07/25/science/ai-math-alphaproof-deepmind.html">the original</a> on July 29, 2024.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=New+York+Times&rft.atitle=Move+Over%2C+Mathematicians%2C+Here+Comes+AlphaProof&rft.date=2024-07-25&rft.aulast=Roberts&rft.aufirst=Siobhan&rft_id=https%3A%2F%2Fwww.nytimes.com%2F2024%2F07%2F25%2Fscience%2Fai-math-alphaproof-deepmind.html&rfr_id=info%3Asid%2Fen.wikipedia.org%3ALean+%28proof+assistant%29" class="Z3988"></span></span> </li> </ol></div></div> <div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Lean_(proof_assistant)&action=edit&section=11" title="Edit section: External links"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a rel="nofollow" class="external text" href="https://leanprover.github.io/">Lean Website</a></li> <li><a rel="nofollow" class="external text" href="https://leanprover-community.github.io/">Lean Community Website</a></li> <li><a rel="nofollow" class="external text" href="https://lean-fro.org">Lean FRO</a></li> <li><a rel="nofollow" class="external text" href="https://adam.math.hhu.de/#/g/leanprover-community/nng4">The Natural Number Game- An interactive tutorial to learn lean</a></li></ul> <div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1129693374">.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}</style><style data-mw-deduplicate="TemplateStyles:r1236075235">.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}</style></div><div role="navigation" class="navbox" aria-labelledby="Microsoft_free_and_open-source_software_(FOSS)" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><style data-mw-deduplicate="TemplateStyles:r1239400231">.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}</style><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Microsoft_FOSS" title="Template:Microsoft FOSS"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Microsoft_FOSS" title="Template talk:Microsoft FOSS"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Microsoft_FOSS" title="Special:EditPage/Template:Microsoft FOSS"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Microsoft_free_and_open-source_software_(FOSS)" style="font-size:114%;margin:0 4em"><a href="/wiki/Microsoft" title="Microsoft">Microsoft</a> <a href="/wiki/Free_and_open-source_software" title="Free and open-source software">free and open-source software (FOSS)</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Overview</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_and_open_source" title="Microsoft and open source">Microsoft and open source</a></li> <li><a href="/wiki/Shared_Source_Initiative" title="Shared Source Initiative">Shared Source Initiative</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Software</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Applications</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/3D_Movie_Maker" title="3D Movie Maker">3D Movie Maker</a></li> <li><a href="/wiki/Atom_(text_editor)" title="Atom (text editor)">Atom</a></li> <li><a href="/wiki/Conference_XP" title="Conference XP">Conference XP</a></li> <li><a href="/wiki/Family.Show" title="Family.Show">Family.Show</a></li> <li><a href="/wiki/File_Manager_(Windows)" class="mw-redirect" title="File Manager (Windows)">File Manager</a></li> <li><a href="/wiki/Open_Live_Writer" title="Open Live Writer">Open Live Writer</a></li> <li><a href="/wiki/Microsoft_PowerToys" title="Microsoft PowerToys">Microsoft PowerToys</a></li> <li><a href="/wiki/Windows_Terminal" title="Windows Terminal">Terminal</a></li> <li><a href="/wiki/Windows_Calculator" title="Windows Calculator">Windows Calculator</a></li> <li><a href="/wiki/Windows_Console" title="Windows Console">Windows Console</a></li> <li><a href="/wiki/Windows_Package_Manager" title="Windows Package Manager">Windows Package Manager</a></li> <li><a href="/wiki/WorldWide_Telescope" title="WorldWide Telescope">WorldWide Telescope</a></li> <li><a href="/wiki/XML_Notepad" title="XML Notepad">XML Notepad</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Video games</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Allegiance_(video_game)" title="Allegiance (video game)">Allegiance</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Programming<br />languages</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Bosque_(programming_language)" title="Bosque (programming language)">Bosque</a></li> <li><a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a></li> <li><a href="/wiki/Dafny" title="Dafny">Dafny</a></li> <li><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></li> <li><a href="/wiki/F*_(programming_language)" title="F* (programming language)">F*</a></li> <li><a href="/wiki/GW-BASIC" title="GW-BASIC">GW-BASIC</a></li> <li><a href="/wiki/IronPython" title="IronPython">IronPython</a></li> <li><a href="/wiki/IronRuby" title="IronRuby">IronRuby</a></li> <li><a class="mw-selflink selflink">Lean</a></li> <li><a href="/wiki/P_(programming_language)" title="P (programming language)">P</a></li> <li><a href="/wiki/Microsoft_Power_Fx" title="Microsoft Power Fx">Power Fx</a></li> <li><a href="/wiki/PowerShell" title="PowerShell">PowerShell</a></li> <li><a href="/wiki/Project_Verona" title="Project Verona">Project Verona</a></li> <li><a href="/wiki/Q_Sharp" title="Q Sharp">Q#</a></li> <li><a href="/wiki/Microsoft_Small_Basic" title="Microsoft Small Basic">Small Basic Online</a></li> <li><a href="/wiki/TypeScript" title="TypeScript">TypeScript</a></li> <li><a href="/wiki/Visual_Basic_.NET" class="mw-redirect" title="Visual Basic .NET">Visual Basic</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Frameworks,<br />development tools</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/.NET" title=".NET">.NET</a></li> <li><a href="/wiki/.NET_Framework" title=".NET Framework">.NET Framework</a></li> <li><a href="/wiki/.NET_Gadgeteer" title=".NET Gadgeteer">.NET Gadgeteer</a></li> <li><a href="/wiki/.NET_MAUI" class="mw-redirect" title=".NET MAUI">.NET MAUI</a></li> <li><a href="/wiki/.NET_Micro_Framework" title=".NET Micro Framework">.NET Micro Framework</a></li> <li><a href="/wiki/AirSim" title="AirSim">AirSim</a></li> <li><a href="/wiki/ASP.NET" title="ASP.NET">ASP.NET</a></li> <li><a href="/wiki/ASP.NET_AJAX" title="ASP.NET AJAX">ASP.NET AJAX</a></li> <li><a href="/wiki/ASP.NET_Core" title="ASP.NET Core">ASP.NET Core</a></li> <li><a href="/wiki/ASP.NET_MVC" title="ASP.NET MVC">ASP.NET MVC</a></li> <li><a href="/wiki/ASP.NET_Razor" title="ASP.NET Razor">ASP.NET Razor</a></li> <li><a href="/wiki/ASP.NET_Web_Forms" title="ASP.NET Web Forms">ASP.NET Web Forms</a></li> <li><a href="/wiki/Avalonia_(software_framework)" title="Avalonia (software framework)">Avalonia</a></li> <li><a href="/wiki/Babylon.js" title="Babylon.js">Babylon.js</a></li> <li><a href="/wiki/BitFunnel" title="BitFunnel">BitFunnel</a></li> <li><a href="/wiki/Blazor" title="Blazor">Blazor</a></li> <li><a href="/wiki/C%2B%2B/WinRT" title="C++/WinRT">C++/WinRT</a></li> <li><a href="/wiki/Confidential_Consortium_Framework" title="Confidential Consortium Framework">CCF</a></li> <li><a href="/wiki/Chakra_(JavaScript_engine)" title="Chakra (JavaScript engine)">ChakraCore</a></li> <li><a href="/wiki/CLR_Profiler" title="CLR Profiler">CLR Profiler</a></li> <li><a href="/wiki/Dapr" title="Dapr">Dapr</a></li> <li><a href="/wiki/DeepSpeed" title="DeepSpeed">DeepSpeed</a></li> <li><a href="/wiki/DiskSpd" title="DiskSpd">DiskSpd</a></li> <li><a href="/wiki/Dryad_(programming)" title="Dryad (programming)">Dryad</a></li> <li><a href="/wiki/Dynamic_Language_Runtime" title="Dynamic Language Runtime">Dynamic Language Runtime</a></li> <li><a href="/wiki/EBPF_on_Windows" class="mw-redirect" title="EBPF on Windows">eBPF on Windows</a></li> <li><a href="/wiki/Electron_(software_framework)" title="Electron (software framework)">Electron</a></li> <li><a href="/wiki/Entity_Framework" title="Entity Framework">Entity Framework</a></li> <li><a href="/wiki/Fluent_Design_System" title="Fluent Design System">Fluent Design System</a></li> <li><a href="/wiki/Fluid_Framework" title="Fluid Framework">Fluid Framework</a></li> <li><a href="/wiki/Infer.NET" title="Infer.NET">Infer.NET</a></li> <li><a href="/wiki/LightGBM" title="LightGBM">LightGBM</a></li> <li><a href="/wiki/Managed_Extensibility_Framework" title="Managed Extensibility Framework">Managed Extensibility Framework</a></li> <li><a href="/wiki/Microsoft_Automatic_Graph_Layout" title="Microsoft Automatic Graph Layout">Microsoft Automatic Graph Layout</a></li> <li><a href="/wiki/Microsoft_C%2B%2B_Standard_Library" class="mw-redirect" title="Microsoft C++ Standard Library">Microsoft C++ Standard Library</a></li> <li><a href="/wiki/Microsoft_Cognitive_Toolkit" title="Microsoft Cognitive Toolkit">Microsoft Cognitive Toolkit</a></li> <li><a href="/wiki/Metro_(design_language)" title="Metro (design language)">Microsoft Design Language</a></li> <li><a href="/wiki/Microsoft_Detours" title="Microsoft Detours">Microsoft Detours</a></li> <li><a href="/wiki/Microsoft_Enterprise_Library" title="Microsoft Enterprise Library">Microsoft Enterprise Library</a></li> <li><a href="/wiki/Microsoft_SEAL" title="Microsoft SEAL">Microsoft SEAL</a></li> <li><a href="/wiki/Mimalloc" title="Mimalloc">mimalloc</a></li> <li><a href="/wiki/Mixed_Reality_Toolkit" title="Mixed Reality Toolkit">Mixed Reality Toolkit</a></li> <li><a href="/wiki/ML.NET" title="ML.NET">ML.NET</a></li> <li><a href="/wiki/Mod_mono" title="Mod mono">mod_mono</a></li> <li><a href="/wiki/Mono_(software)" title="Mono (software)">Mono</a></li> <li><a href="/wiki/MonoDevelop" title="MonoDevelop">MonoDevelop</a></li> <li><a href="/wiki/MSBuild" title="MSBuild">MSBuild</a></li> <li><a href="/wiki/MsQuic" title="MsQuic">MsQuic</a></li> <li><a href="/wiki/Neural_Network_Intelligence" title="Neural Network Intelligence">Neural Network Intelligence</a></li> <li><a href="/wiki/Npm" title="Npm">npm</a></li> <li><a href="/wiki/NuGet" title="NuGet">NuGet</a></li> <li><a href="/wiki/OneFuzz" title="OneFuzz">OneFuzz</a></li> <li><a href="/wiki/Open_Management_Infrastructure" title="Open Management Infrastructure">Open Management Infrastructure</a></li> <li><a href="/wiki/Open_Neural_Network_Exchange" title="Open Neural Network Exchange">Open Neural Network Exchange</a></li> <li><a href="/wiki/Open_Service_Mesh" title="Open Service Mesh">Open Service Mesh</a></li> <li><a href="/wiki/Open_XML_SDK" class="mw-redirect" title="Open XML SDK">Open XML SDK</a></li> <li><a href="/wiki/Orleans_(software_framework)" title="Orleans (software framework)">Orleans</a></li> <li><a href="/wiki/Playwright_(software)" title="Playwright (software)">Playwright</a></li> <li><a href="/wiki/ProcDump" title="ProcDump">ProcDump</a></li> <li><a href="/wiki/Process_Monitor" title="Process Monitor">ProcMon</a></li> <li><a href="/wiki/Python_Tools_for_Visual_Studio" title="Python Tools for Visual Studio">Python Tools for Visual Studio</a></li> <li><a href="/wiki/R_Tools_for_Visual_Studio" title="R Tools for Visual Studio">R Tools for Visual Studio</a></li> <li><a href="/wiki/RecursiveExtractor" class="mw-redirect" title="RecursiveExtractor">RecursiveExtractor</a></li> <li><a href="/wiki/Roslyn_(compiler)" title="Roslyn (compiler)">Roslyn</a></li> <li><a href="/wiki/Sandcastle_(software)" title="Sandcastle (software)">Sandcastle</a></li> <li><a href="/wiki/SignalR" title="SignalR">SignalR</a></li> <li><a href="/wiki/StyleCop" title="StyleCop">StyleCop</a></li> <li><a href="/wiki/SVNBridge" title="SVNBridge">SVNBridge</a></li> <li><a href="/wiki/T2_Temporal_Prover" title="T2 Temporal Prover">T2 Temporal Prover</a></li> <li><a href="/wiki/Text_Template_Transformation_Toolkit" title="Text Template Transformation Toolkit">Text Template Transformation Toolkit</a></li> <li><a href="/wiki/TLA%2B_Toolbox" class="mw-redirect" title="TLA+ Toolbox">TLA+ Toolbox</a></li> <li><a href="/wiki/U-Prove" title="U-Prove">U-Prove</a></li> <li><a href="/wiki/Vcpkg" title="Vcpkg">vcpkg</a></li> <li><a href="/wiki/Virtual_File_System_for_Git" title="Virtual File System for Git">Virtual File System for Git</a></li> <li><a href="/wiki/Voldemort_(distributed_data_store)" title="Voldemort (distributed data store)">Voldemort</a></li> <li><a href="/wiki/VoTT" title="VoTT">VoTT</a></li> <li><a href="/wiki/Vowpal_Wabbit" title="Vowpal Wabbit">Vowpal Wabbit</a></li> <li><a href="/wiki/Windows_App_SDK" title="Windows App SDK">Windows App SDK</a></li> <li><a href="/wiki/Windows_Communication_Foundation" title="Windows Communication Foundation">Windows Communication Foundation</a></li> <li><a href="/wiki/Windows_Driver_Frameworks" title="Windows Driver Frameworks">Windows Driver Frameworks</a> <ul><li><a href="/wiki/Kernel-Mode_Driver_Framework" title="Kernel-Mode Driver Framework">KMDF</a></li> <li><a href="/wiki/User-Mode_Driver_Framework" title="User-Mode Driver Framework">UMDF</a></li></ul></li> <li><a href="/wiki/Windows_Forms" title="Windows Forms">Windows Forms</a></li> <li><a href="/wiki/Windows_Presentation_Foundation" title="Windows Presentation Foundation">Windows Presentation Foundation</a></li> <li><a href="/wiki/Windows_Template_Library" title="Windows Template Library">Windows Template Library</a></li> <li><a href="/wiki/Windows_UI_Library" title="Windows UI Library">Windows UI Library</a></li> <li><a href="/wiki/WinJS" title="WinJS">WinJS</a></li> <li><a href="/wiki/WinObjC" class="mw-redirect" title="WinObjC">WinObjC</a></li> <li><a href="/wiki/WiX" title="WiX">WiX</a></li> <li><a href="/wiki/XDP_for_Windows" class="mw-redirect" title="XDP for Windows">XDP for Windows</a></li> <li><a href="/wiki/XSP_(software)" title="XSP (software)">XSP</a></li> <li><a href="/wiki/XUnit.net" title="XUnit.net">xUnit.net</a></li> <li><a href="/wiki/Z3_Theorem_Prover" title="Z3 Theorem Prover">Z3 Theorem Prover</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Operating systems</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/MS-DOS" title="MS-DOS">MS-DOS</a> (v1.25, v2.0 & v4.0)</li> <li><a href="/wiki/Barrelfish_(operating_system)" title="Barrelfish (operating system)">Barrelfish</a></li> <li><a href="/wiki/SONiC_(operating_system)" title="SONiC (operating system)">SONiC</a></li> <li><a href="/wiki/Azure_Linux" title="Azure Linux">Azure Linux</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/ChronoZoom" title="ChronoZoom">ChronoZoom</a></li> <li><a href="/wiki/Extensible_Storage_Engine" title="Extensible Storage Engine">Extensible Storage Engine</a></li> <li><a href="/wiki/FlexWiki" class="mw-redirect" title="FlexWiki">FlexWiki</a></li> <li><a href="/wiki/FourQ" title="FourQ">FourQ</a></li> <li><a href="/wiki/Gollum_(software)" title="Gollum (software)">Gollum</a></li> <li><a href="/wiki/Project_Mu" class="mw-redirect" title="Project Mu">Project Mu</a></li> <li><a href="/wiki/ReactiveX" title="ReactiveX">ReactiveX</a></li> <li><a href="/wiki/SILK" title="SILK">SILK</a></li> <li><a href="/wiki/TLAPS" class="mw-redirect" title="TLAPS">TLAPS</a></li> <li><a href="/wiki/TPM_2.0_Reference_Implementation" class="mw-redirect" title="TPM 2.0 Reference Implementation">TPM 2.0 Reference Implementation</a></li> <li><a href="/wiki/WikiBhasha" title="WikiBhasha">WikiBhasha</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Open-source_license" title="Open-source license">Licenses</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Public_License" class="mw-redirect" title="Microsoft Public License">Microsoft Public License</a></li> <li><a href="/wiki/Microsoft_Reciprocal_License" class="mw-redirect" title="Microsoft Reciprocal License">Microsoft Reciprocal License</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Forge_(software)" title="Forge (software)">Forges</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/CodePlex" title="CodePlex">CodePlex</a></li> <li><a href="/wiki/GitHub" title="GitHub">GitHub</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/.NET_Foundation" title=".NET Foundation">.NET Foundation</a></li> <li><a href="/wiki/F_Sharp_Software_Foundation" title="F Sharp Software Foundation">F# Software Foundation</a></li> <li><a href="/wiki/Microsoft_Open_Specification_Promise" title="Microsoft Open Specification Promise">Microsoft Open Specification Promise</a></li> <li><a href="/wiki/Open_Letter_to_Hobbyists" class="mw-redirect" title="Open Letter to Hobbyists">Open Letter to Hobbyists</a></li> <li><a href="/wiki/Open_Source_Security_Foundation" title="Open Source Security Foundation">Open Source Security Foundation</a></li> <li><a href="/wiki/Outercurve_Foundation" title="Outercurve Foundation">Outercurve Foundation</a></li></ul> </div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="noviewer" typeof="mw:File"><span title="Category"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/23px-Symbol_category_class.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/31px-Symbol_category_class.svg.png 2x" data-file-width="180" data-file-height="185" /></span></span> <a href="/wiki/Category:Microsoft_free_software" title="Category:Microsoft free software">Category</a></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox" aria-labelledby="Microsoft_development_tools" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Microsoft_development_tools" title="Template:Microsoft development tools"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Microsoft_development_tools" title="Template talk:Microsoft development tools"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Microsoft_development_tools" title="Special:EditPage/Template:Microsoft development tools"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Microsoft_development_tools" style="font-size:114%;margin:0 4em">Microsoft development tools</div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Development<br />environments</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Microsoft_Visual_Studio" class="mw-redirect" title="Microsoft Visual Studio">Visual Studio</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Visual_Studio_Code" title="Visual Studio Code">Code</a></li> <li><a href="/wiki/Microsoft_Visual_Studio_Express" title="Microsoft Visual Studio Express">Express</a></li> <li><a href="/wiki/VSTS_Profiler" title="VSTS Profiler">Team System Profiler</a></li> <li><a href="/wiki/Visual_Studio_Tools_for_Applications" title="Visual Studio Tools for Applications">Tools for Applications</a></li> <li><a href="/wiki/Visual_Studio_Tools_for_Office" title="Visual Studio Tools for Office">Tools for Office</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Others</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Blend" title="Microsoft Blend">Blend</a></li> <li><a href="/wiki/Microsoft_Expression_Web" title="Microsoft Expression Web">Expression Web</a></li> <li><a href="/wiki/FxCop" title="FxCop">FxCop</a></li> <li><a href="/wiki/GW-BASIC" title="GW-BASIC">GW-BASIC</a></li> <li><a href="/wiki/Microsoft_MACRO-80" title="Microsoft MACRO-80">MACRO-80</a></li> <li><a href="/wiki/Microsoft_Macro_Assembler" title="Microsoft Macro Assembler">Macro Assembler</a></li> <li><a href="/wiki/MSBuild" title="MSBuild">MSBuild</a></li> <li><a href="/wiki/Microsoft_Pascal" title="Microsoft Pascal">Pascal</a></li> <li><a href="/wiki/QuickBASIC" title="QuickBASIC">QuickBASIC</a> <ul><li><a href="/wiki/QBasic" title="QBasic">QBasic</a></li></ul></li> <li><a href="/wiki/QuickC" title="QuickC">QuickC</a></li> <li><a href="/wiki/Microsoft_Robotics_Developer_Studio" title="Microsoft Robotics Developer Studio">Robotics Developer Studio</a></li> <li><a href="/wiki/Roslyn_(compiler)" title="Roslyn (compiler)">Roslyn</a></li> <li><a href="/wiki/Microsoft_SharePoint_Designer" title="Microsoft SharePoint Designer">SharePoint Designer</a> <ul><li><a href="/wiki/Microsoft_FrontPage" title="Microsoft FrontPage">FrontPage</a></li></ul></li> <li><a href="/wiki/Microsoft_Small_Basic" title="Microsoft Small Basic">Small Basic</a></li> <li><a href="/wiki/Microsoft_WebMatrix" title="Microsoft WebMatrix">WebMatrix</a></li> <li><a href="/wiki/Windows_App_SDK" title="Windows App SDK">Windows App SDK</a></li> <li><a href="/wiki/Windows_App_Studio" title="Windows App Studio">Windows App Studio</a></li> <li><a href="/wiki/Microsoft_Windows_SDK" title="Microsoft Windows SDK">Windows SDK</a> <ul><li><a href="/wiki/CLR_Profiler" title="CLR Profiler">CLR Profiler</a></li> <li><a href="/wiki/ILAsm" title="ILAsm">ILAsm</a></li> <li><a href="/wiki/Native_Image_Generator" title="Native Image Generator">Native Image Generator</a></li> <li><a href="/wiki/WinDiff" title="WinDiff">WinDiff</a></li> <li><a href="/wiki/XAMLPad" class="mw-redirect" title="XAMLPad">XAMLPad</a></li></ul></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Languages</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Dynamics_AX" class="mw-redirect" title="Microsoft Dynamics AX">Dynamics AX</a></li> <li><a href="/wiki/Microsoft_BASIC" title="Microsoft BASIC">BASIC</a></li> <li>Visual Basic <ul><li><a href="/wiki/Visual_Basic_(classic)" title="Visual Basic (classic)">legacy</a></li> <li><a href="/wiki/Visual_Basic_.NET" class="mw-redirect" title="Visual Basic .NET">VB.NET</a></li> <li><a href="/wiki/Visual_Basic_for_Applications" title="Visual Basic for Applications">VBA</a></li> <li><a href="/wiki/VBScript" title="VBScript">VBScript</a></li></ul></li> <li><a href="/wiki/Bosque_(programming_language)" title="Bosque (programming language)">Bosque</a></li> <li><a href="/wiki/Microsoft_Visual_C%2B%2B" title="Microsoft Visual C++">Visual C++</a> <ul><li><a href="/wiki/C%2B%2B/CX" title="C++/CX">C++/CX</a></li> <li><a href="/wiki/C%2B%2B/CLI" title="C++/CLI">C++/CLI</a></li> <li><a href="/wiki/Managed_Extensions_for_C%2B%2B" title="Managed Extensions for C++">Managed C++</a></li> <li><a href="/wiki/C%2B%2B/WinRT" title="C++/WinRT">C++/WinRT</a></li></ul></li> <li><a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a></li> <li><a href="/wiki/C/AL" title="C/AL">C/AL</a></li> <li><a href="/wiki/Dafny" title="Dafny">Dafny</a></li> <li><a href="/wiki/Dexterity_(programming_language)" title="Dexterity (programming language)">Dexterity</a></li> <li><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></li> <li><a href="/wiki/F*_(programming_language)" title="F* (programming language)">F*</a></li> <li><a href="/wiki/Visual_FoxPro" title="Visual FoxPro">Visual FoxPro</a></li> <li><a href="/wiki/Java_(programming_language)" title="Java (programming language)">Java</a> <ul><li><a href="/wiki/Visual_J%2B%2B" title="Visual J++">J++</a></li> <li><a href="/wiki/Visual_J_Sharp" title="Visual J Sharp">J#</a></li></ul></li> <li><a href="/wiki/JavaScript" title="JavaScript">JavaScript</a> <ul><li><a href="/wiki/TypeScript" title="TypeScript">TypeScript</a></li> <li><a href="/wiki/JScript" title="JScript">JScript</a></li></ul></li> <li><a href="/wiki/IronPython" title="IronPython">IronPython</a></li> <li><a href="/wiki/IronRuby" title="IronRuby">IronRuby</a></li> <li><a class="mw-selflink selflink">Lean</a></li> <li><a href="/wiki/P_(programming_language)" title="P (programming language)">P</a></li> <li><a href="/wiki/Microsoft_Power_Fx" title="Microsoft Power Fx">Power Fx</a></li> <li><a href="/wiki/PowerShell" title="PowerShell">PowerShell</a></li> <li><a href="/wiki/Project_Verona" title="Project Verona">Project Verona</a></li> <li><a href="/wiki/Q_Sharp" title="Q Sharp">Q#</a></li> <li><a href="/wiki/Microsoft_Small_Basic" title="Microsoft Small Basic">Small Basic</a></li> <li><a href="/wiki/Microsoft_Visual_Programming_Language" title="Microsoft Visual Programming Language">VPL</a></li> <li><a href="/wiki/Extensible_Application_Markup_Language" title="Extensible Application Markup Language">XAML</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">APIs and<br />frameworks</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">Native</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Windows_API" title="Windows API">Windows API</a></li> <li><a href="/wiki/Microsoft_Silverlight" title="Microsoft Silverlight">Silverlight</a></li> <li><a href="/wiki/Microsoft_XNA" title="Microsoft XNA">XNA</a></li> <li><a href="/wiki/DirectX" title="DirectX">DirectX</a> <ul><li><a href="/wiki/Managed_DirectX" title="Managed DirectX">Managed DirectX</a></li></ul></li> <li><a href="/wiki/Universal_Windows_Platform" title="Universal Windows Platform">UWP</a></li> <li><a href="/wiki/Xbox_Development_Kit" title="Xbox Development Kit">Xbox Development Kit</a></li> <li><a href="/wiki/Windows_Installer" title="Windows Installer">Windows Installer</a></li> <li><a href="/wiki/WinUI" class="mw-redirect" title="WinUI">WinUI</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="/wiki/.NET" title=".NET">.NET</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/ASP.NET" title="ASP.NET">ASP.NET</a> <ul><li><a href="/wiki/ASP.NET_Core" title="ASP.NET Core">Core</a></li> <li><a href="/wiki/ASP.NET_AJAX" title="ASP.NET AJAX">AJAX</a></li> <li><a href="/wiki/ASP.NET_Dynamic_Data" title="ASP.NET Dynamic Data">Dynamic Data</a></li> <li><a href="/wiki/ASP.NET_MVC" title="ASP.NET MVC">MVC</a></li> <li><a href="/wiki/ASP.NET_Razor" title="ASP.NET Razor">Razor</a></li> <li><a href="/wiki/ASP.NET_Web_Forms" title="ASP.NET Web Forms">Web Forms</a></li></ul></li> <li><a href="/wiki/ADO.NET" title="ADO.NET">ADO.NET</a> <ul><li><a href="/wiki/Entity_Framework" title="Entity Framework">Entity Framework</a></li></ul></li> <li><a href="/wiki/.NET_MAUI" class="mw-redirect" title=".NET MAUI">MAUI</a></li> <li><a href="/wiki/Windows_CardSpace" title="Windows CardSpace">CardSpace</a></li> <li><a href="/wiki/Windows_Communication_Foundation" title="Windows Communication Foundation">Communication Foundation</a></li> <li><a href="/wiki/Windows_Identity_Foundation" title="Windows Identity Foundation">Identity Foundation</a></li> <li><a href="/wiki/Language_Integrated_Query" title="Language Integrated Query">LINQ</a></li> <li><a href="/wiki/Windows_Presentation_Foundation" title="Windows Presentation Foundation">Presentation Foundation</a></li> <li><a href="/wiki/Windows_Workflow_Foundation" title="Windows Workflow Foundation">Workflow Foundation</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="/wiki/Device_driver" title="Device driver">Device drivers</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Windows_Driver_Kit" title="Windows Driver Kit">WDK</a></li> <li><a href="/wiki/Windows_Driver_Frameworks" title="Windows Driver Frameworks">WDF</a> <ul><li><a href="/wiki/Kernel-Mode_Driver_Framework" title="Kernel-Mode Driver Framework">KMDF</a></li> <li><a href="/wiki/User-Mode_Driver_Framework" title="User-Mode Driver Framework">UMDF</a></li></ul></li> <li><a href="/wiki/Windows_Hardware_Lab_Kit" title="Windows Hardware Lab Kit">Windows HLK</a></li> <li><a href="/wiki/Windows_Driver_Model" title="Windows Driver Model">WDM</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Database</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="/wiki/Microsoft_SQL_Server" title="Microsoft SQL Server">SQL Server</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/SQL_Server_Express" title="SQL Server Express">Express</a></li> <li><a href="/wiki/SQL_Server_Compact" title="SQL Server Compact">Compact</a></li> <li><a href="/wiki/SQL_Server_Management_Studio" title="SQL Server Management Studio">Management Studio</a></li> <li><a href="/wiki/Business_Intelligence_Development_Studio" title="Business Intelligence Development Studio">Business Intelligence Development Studio</a></li> <li><a href="/wiki/MSDE" title="MSDE">MSDE</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">SQL services</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Analysis_Services" title="Microsoft Analysis Services">Analysis</a></li> <li><a href="/wiki/SQL_Server_Reporting_Services" title="SQL Server Reporting Services">Reporting</a></li> <li><a href="/wiki/SQL_Server_Integration_Services" title="SQL Server Integration Services">Integration</a></li> <li><a href="/wiki/SQL_Server_Notification_Services" title="SQL Server Notification Services">Notification</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">Other</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Visual_FoxPro" title="Visual FoxPro">Visual FoxPro</a></li> <li><a href="/wiki/Microsoft_Access" title="Microsoft Access">Microsoft Access</a></li> <li><a href="/wiki/Access_Database_Engine" title="Access Database Engine">Access Database Engine</a></li> <li><a href="/wiki/Extensible_Storage_Engine" title="Extensible Storage Engine">Extensible Storage Engine</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Source control</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Visual_SourceSafe" title="Microsoft Visual SourceSafe">Visual SourceSafe</a></li> <li><a href="/wiki/Azure_DevOps_Server#TFVC" title="Azure DevOps Server">Team Foundation Version Control</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Testing and<br />debugging</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/CodeView" title="CodeView">CodeView</a></li> <li><a href="/wiki/OneFuzz" title="OneFuzz">OneFuzz</a></li> <li><a href="/wiki/Playwright_(software)" title="Playwright (software)">Playwright</a></li> <li><a href="/wiki/Microsoft_Script_Debugger" title="Microsoft Script Debugger">Script Debugger</a></li> <li><a href="/wiki/WinDbg" title="WinDbg">WinDbg</a></li> <li><a href="/wiki/XUnit.net" title="XUnit.net">xUnit.net</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Delivery</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Active_Setup" title="Active Setup">Active Setup</a></li> <li><a href="/wiki/ClickOnce" title="ClickOnce">ClickOnce</a></li> <li><a href="/wiki/Npm_(software)" class="mw-redirect" title="Npm (software)">npm</a></li> <li><a href="/wiki/NuGet" title="NuGet">NuGet</a></li> <li><a href="/wiki/Vcpkg" title="Vcpkg">vcpkg</a></li> <li><a href="/wiki/Web_Platform_Installer" title="Web Platform Installer">Web Platform Installer</a></li> <li><a href="/wiki/Windows_Installer" title="Windows Installer">Windows Installer</a> <ul><li><a href="/wiki/WiX" title="WiX">WiX</a></li></ul></li> <li><a href="/wiki/Windows_Package_Manager" title="Windows Package Manager">Windows Package Manager</a></li> <li><a href="/wiki/Microsoft_Store" title="Microsoft Store">Microsoft Store</a></li></ul> </div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="noviewer" typeof="mw:File"><span title="Category"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/23px-Symbol_category_class.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/31px-Symbol_category_class.svg.png 2x" data-file-width="180" data-file-height="185" /></span></span> <a href="/wiki/Category:Microsoft_development_tools" title="Category:Microsoft development tools">Category</a></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox" aria-labelledby="Microsoft_Research_(MSR)" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Microsoft_Research" title="Template:Microsoft Research"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Microsoft_Research" title="Template talk:Microsoft Research"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Microsoft_Research" title="Special:EditPage/Template:Microsoft Research"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Microsoft_Research_(MSR)" style="font-size:114%;margin:0 4em"><a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research (MSR)</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Main<br />projects</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Languages, compilers</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Bartok_(compiler)" title="Bartok (compiler)">Bartok</a></li> <li><a href="/wiki/Bosque_(programming_language)" title="Bosque (programming language)">Bosque</a></li> <li><a href="/wiki/C%CF%89" class="mw-redirect" title="Cω">Cω</a></li> <li><a href="/wiki/F*_(programming_language)" title="F* (programming language)">F*</a></li> <li><a class="mw-selflink selflink">Lean</a></li> <li><a href="/wiki/P_(programming_language)" title="P (programming language)">P</a></li> <li><a href="/wiki/Project_Verona" title="Project Verona">Project Verona</a></li> <li><a href="/wiki/Microsoft_Phoenix" title="Microsoft Phoenix">Phoenix</a></li> <li><a href="/wiki/Polyphonic_C_Sharp" class="mw-redirect" title="Polyphonic C Sharp">Polyphonic C#</a></li> <li><a href="/wiki/SecPAL" title="SecPAL">SecPAL</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Distributed_computing" title="Distributed computing">Distributed</a>–<a href="/wiki/Grid_computing" title="Grid computing">grid computing</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/BitVault" title="BitVault">BitVault</a></li> <li><a href="/wiki/Confidential_Consortium_Framework" title="Confidential Consortium Framework">Confidential Consortium Framework</a></li> <li><a href="/wiki/DeepSpeed" title="DeepSpeed">DeepSpeed</a></li> <li><a href="/wiki/Orleans_(software_framework)" title="Orleans (software framework)">Orleans</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Internet" title="Internet">Internet</a>, <a href="/wiki/Computer_network" title="Computer network">networking</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/AjaxView" title="AjaxView">AjaxView</a></li> <li><a href="/wiki/Avalanche_(P2P)" title="Avalanche (P2P)">Avalanche</a></li> <li><a href="/wiki/Conference_XP" title="Conference XP">Conference XP</a></li> <li><a href="/wiki/Gazelle_(web_browser)" title="Gazelle (web browser)">Gazelle</a></li> <li><a href="/wiki/HoneyMonkey" title="HoneyMonkey">HoneyMonkey</a></li> <li><a href="/wiki/Penny_Black_(research_project)" title="Penny Black (research project)">Penny Black</a></li> <li><a href="/wiki/Wallop" title="Wallop">Wallop</a></li> <li><a href="/wiki/WikiBhasha" title="WikiBhasha">WikiBhasha</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other projects</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Automatic_Graph_Layout" title="Microsoft Automatic Graph Layout">Automatic Graph Layout</a></li> <li><a href="/wiki/Microsoft_Cognitive_Toolkit" title="Microsoft Cognitive Toolkit">Cognitive Toolkit</a></li> <li><a href="/wiki/Project_Digits" title="Project Digits">Digits</a></li> <li><a href="/wiki/Microsoft_Holoportation" title="Microsoft Holoportation">Holoportation</a></li> <li><a href="/wiki/IllumiRoom" title="IllumiRoom">IllumiRoom</a></li> <li><a href="/wiki/Image_Composite_Editor" title="Image Composite Editor">Image Composite Editor</a></li> <li><a href="/wiki/Infer.NET" title="Infer.NET">Infer.NET</a></li> <li><a href="/wiki/LightGBM" title="LightGBM">LightGBM</a></li> <li><a href="/wiki/LiveStation" title="LiveStation">LiveStation</a></li> <li><a href="/wiki/MyLifeBits" title="MyLifeBits">MyLifeBits</a></li> <li><a href="/wiki/Neural_Network_Intelligence" title="Neural Network Intelligence">Neural Network Intelligence</a></li> <li><a href="/wiki/NodeXL" title="NodeXL">NodeXL</a></li> <li><a href="/wiki/OneFuzz" title="OneFuzz">OneFuzz</a></li> <li><a href="/wiki/PhotoDNA" title="PhotoDNA">PhotoDNA</a></li> <li><a href="/wiki/Microsoft_SEAL" title="Microsoft SEAL">SEAL</a></li> <li><a href="/wiki/SLAM_project" title="SLAM project">SLAM</a></li> <li><a href="/wiki/T2_Temporal_Prover" title="T2 Temporal Prover">T2 Temporal Prover</a></li> <li><a href="/wiki/WorldWide_Telescope" title="WorldWide Telescope">WorldWide Telescope</a></li> <li><a href="/wiki/Z3_Theorem_Prover" title="Z3 Theorem Prover">Z3 Theorem Prover</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Operating_system" title="Operating system">Operating systems</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Barrelfish_(operating_system)" title="Barrelfish (operating system)">Barrelfish</a></li> <li><a href="/wiki/HomeOS" title="HomeOS">HomeOS</a></li> <li><a href="/wiki/Midori_(operating_system)" title="Midori (operating system)">Midori</a></li> <li><a href="/wiki/Singularity_(operating_system)" title="Singularity (operating system)">Singularity</a></li> <li><a href="/wiki/Verve_(operating_system)" title="Verve (operating system)">Verve</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/API" title="API">APIs</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Accelerator_(library)" title="Accelerator (library)">Accelerator</a></li> <li><a href="/wiki/Dryad_(programming)" title="Dryad (programming)">Dryad</a></li> <li><a href="/wiki/Joins_(concurrency_library)" title="Joins (concurrency library)">Joins</a></li> <li><a href="/wiki/Mimalloc" title="Mimalloc">mimalloc</a></li> <li><a href="/wiki/SXM_(transactional_memory)" title="SXM (transactional memory)">SXM</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Launched as products</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a></li> <li><a href="/wiki/Microsoft_Comic_Chat" title="Microsoft Comic Chat">Comic Chat</a></li> <li><a href="/wiki/Microsoft_Detours" title="Microsoft Detours">Detours</a></li> <li><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></li> <li><a href="/wiki/Windows_Desktop_Gadgets" title="Windows Desktop Gadgets">Sideshow</a></li> <li><a href="/wiki/Microsoft_PixelSense" title="Microsoft PixelSense">PixelSense</a> (<a href="/wiki/TouchLight" title="TouchLight">TouchLight</a>)</li> <li><a href="/wiki/Microsoft_SenseCam" title="Microsoft SenseCam">SenseCam</a></li> <li><a href="/wiki/ClearType" title="ClearType">ClearType</a></li> <li><a href="/wiki/Group_Shot" title="Group Shot">Group Shot</a></li> <li><a href="/wiki/Allegiance_(video_game)" title="Allegiance (video game)">Allegiance</a></li> <li><a href="/wiki/TrueSkill" title="TrueSkill">TrueSkill</a></li> <li><a href="/wiki/Microsoft_Songsmith" class="mw-redirect" title="Microsoft Songsmith">Songsmith</a></li> <li><a href="/wiki/Xbox" title="Xbox">Xbox</a> <ul><li><a href="/wiki/Kinect" title="Kinect">Kinect</a></li></ul></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">MSR Labs<br />applied<br />research</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Microsoft_Live_Labs" title="Microsoft Live Labs">Live Labs</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Current</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Live_Labs_Pivot" title="Microsoft Live Labs Pivot">Pivot</a></li> <li><a href="/wiki/Seadragon_Software" title="Seadragon Software">Seadragon</a> <ul><li><a href="/wiki/Deep_Zoom" title="Deep Zoom">Deep Zoom</a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Discontinued</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Live_Labs_Deepfish" title="Microsoft Live Labs Deepfish">Deepfish</a></li> <li><a href="/wiki/Microsoft_Live_Labs_Listas" title="Microsoft Live Labs Listas">Listas</a></li> <li><a href="/wiki/Live_Clipboard" title="Live Clipboard">Live Clipboard</a></li> <li><a href="/wiki/Photosynth" title="Photosynth">Photosynth</a></li> <li><a href="/wiki/Microsoft_Live_Labs_Volta" title="Microsoft Live Labs Volta">Volta</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Microsoft_FUSE_Labs" title="Microsoft FUSE Labs">FUSE Labs</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Docs.com" title="Docs.com">Docs.com</a></li> <li><a href="/wiki/Kodu_Game_Lab" title="Kodu Game Lab">Kodu</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other labs</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Academic_Search" title="Microsoft Academic Search">Academic Search</a></li> <li><a href="/wiki/Microsoft_adCenter_Labs" title="Microsoft adCenter Labs">adCenter Labs</a></li> <li><a href="/wiki/Microsoft_Office" title="Microsoft Office">Office Labs</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="noviewer" typeof="mw:File"><span title="Category"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/23px-Symbol_category_class.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/31px-Symbol_category_class.svg.png 2x" data-file-width="180" data-file-height="185" /></span></span> <a href="/wiki/Category:Microsoft_Research" title="Category:Microsoft Research">Category</a></div></td></tr></tbody></table></div>    </div><noscript><img src="https://login.wikimedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Retrieved from "<a dir="ltr" href="https://en.wikipedia.org/w/index.php?title=Lean_(proof_assistant)&oldid=1254178588">https://en.wikipedia.org/w/index.php?title=Lean_(proof_assistant)&oldid=1254178588</a>"</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Help:Category" title="Help:Category">Categories</a>: <ul><li><a href="/wiki/Category:Programming_languages_created_in_2013" title="Category:Programming languages created in 2013">Programming languages created in 2013</a></li><li><a href="/wiki/Category:Proof_assistants" title="Category:Proof assistants">Proof assistants</a></li><li><a href="/wiki/Category:Dependently_typed_languages" title="Category:Dependently typed languages">Dependently typed languages</a></li><li><a href="/wiki/Category:Educational_math_software" title="Category:Educational math software">Educational math software</a></li><li><a href="/wiki/Category:Functional_languages" title="Category:Functional languages">Functional languages</a></li><li><a href="/wiki/Category:Free_and_open-source_software" title="Category:Free and open-source software">Free and open-source software</a></li><li><a href="/wiki/Category:Free_software_programmed_in_C%2B%2B" title="Category:Free software programmed in C++">Free software programmed in C++</a></li><li><a href="/wiki/Category:Microsoft_free_software" title="Category:Microsoft free software">Microsoft free software</a></li><li><a href="/wiki/Category:Microsoft_programming_languages" title="Category:Microsoft programming languages">Microsoft programming languages</a></li><li><a href="/wiki/Category:Microsoft_Research" title="Category:Microsoft Research">Microsoft Research</a></li><li><a href="/wiki/Category:Software_using_the_Apache_license" title="Category:Software using the Apache license">Software using the Apache license</a></li><li><a href="/wiki/Category:Free_mathematics_software" title="Category:Free mathematics software">Free mathematics software</a></li><li><a href="/wiki/Category:Theorem_proving_software_systems" title="Category:Theorem proving software systems">Theorem proving software systems</a></li></ul></div><div id="mw-hidden-catlinks" class="mw-hidden-catlinks mw-hidden-cats-hidden">Hidden categories: <ul><li><a href="/wiki/Category:Articles_with_short_description" title="Category:Articles with short description">Articles with short description</a></li><li><a href="/wiki/Category:Short_description_is_different_from_Wikidata" title="Category:Short description is different from Wikidata">Short description is different from Wikidata</a></li><li><a href="/wiki/Category:All_articles_with_unsourced_statements" title="Category:All articles with unsourced statements">All articles with unsourced statements</a></li><li><a href="/wiki/Category:Articles_with_unsourced_statements_from_October_2023" title="Category:Articles with unsourced statements from October 2023">Articles with unsourced statements from October 2023</a></li></ul></div></div> </div> </main> </div> <div class="mw-footer-container"> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> This page was last edited on 29 October 2024, at 19:37<span class="anonymous-show"> (UTC)</span>.</li> <li id="footer-info-copyright">Text is available under the <a href="/wiki/Wikipedia:Text_of_the_Creative_Commons_Attribution-ShareAlike_4.0_International_License" title="Wikipedia:Text of the Creative Commons Attribution-ShareAlike 4.0 International License">Creative Commons Attribution-ShareAlike 4.0 License</a>; additional terms may apply. By using this site, you agree to the <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Terms_of_Use" class="extiw" title="foundation:Special:MyLanguage/Policy:Terms of Use">Terms of Use</a> and <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy" class="extiw" title="foundation:Special:MyLanguage/Policy:Privacy policy">Privacy Policy</a>. Wikipedia® is a registered trademark of the <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, a non-profit organization.</li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy">Privacy policy</a></li> <li id="footer-places-about"><a href="/wiki/Wikipedia:About">About Wikipedia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikipedia:General_disclaimer">Disclaimers</a></li> <li id="footer-places-contact"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us">Contact Wikipedia</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code of Conduct</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Developers</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/en.wikipedia.org">Statistics</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Cookie statement</a></li> <li id="footer-places-mobileview"><a href="//en.m.wikipedia.org/w/index.php?title=Lean_(proof_assistant)&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Mobile view</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://wikimediafoundation.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/static/images/footer/wikimedia-button.svg" width="84" height="29" alt="Wikimedia Foundation" loading="lazy"></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/w/resources/assets/poweredby_mediawiki.svg" alt="Powered by MediaWiki" width="88" height="31" loading="lazy"></a></li> </ul> </footer> </div> </div> </div> <div class="vector-settings" id="p-dock-bottom"> <ul></ul> </div><script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-f69cdc8f6-mhg5j","wgBackendResponseTime":164,"wgPageParseReport":{"limitreport":{"cputime":"0.670","walltime":"0.926","ppvisitednodes":{"value":3080,"limit":1000000},"postexpandincludesize":{"value":156256,"limit":2097152},"templateargumentsize":{"value":3945,"limit":2097152},"expansiondepth":{"value":27,"limit":100},"expensivefunctioncount":{"value":11,"limit":500},"unstrip-depth":{"value":1,"limit":20},"unstrip-size":{"value":110657,"limit":5000000},"entityaccesscount":{"value":0,"limit":400},"timingprofile":["100.00% 680.114 1 -total"," 33.29% 226.413 1 Template:Reflist"," 23.45% 159.497 10 Template:Navbox"," 22.77% 154.879 2 Template:Infobox"," 17.15% 116.664 1 Template:Microsoft_FOSS"," 15.31% 104.128 1 Template:Infobox_programming_language"," 13.47% 91.636 1 Template:Cite_journal"," 12.35% 84.020 19 Template:Cite_web"," 12.00% 81.613 1 Template:Short_description"," 9.11% 61.931 1 Template:Infobox_software/simple"]},"scribunto":{"limitreport-timeusage":{"value":"0.382","limit":"10.000"},"limitreport-memusage":{"value":7098369,"limit":52428800}},"cachereport":{"origin":"mw-web.codfw.main-f69cdc8f6-4ws7h","timestamp":"20241122153712","ttl":721381,"transientcontent":true}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Lean (proof assistant)","url":"https:\/\/en.wikipedia.org\/wiki\/Lean_(proof_assistant)","sameAs":"http:\/\/www.wikidata.org\/entity\/Q6509476","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q6509476","author":{"@type":"Organization","name":"Contributors to Wikimedia projects"},"publisher":{"@type":"Organization","name":"Wikimedia Foundation, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2020-01-21T21:27:01Z","dateModified":"2024-10-29T19:37:47Z","headline":"software for interactive and automated theorem proving"}</script> </body> </html>