CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> proof assistant in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> proof assistant </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/5013/#Item_14" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="constructivism_realizability_computability">Constructivism, Realizability, Computability</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/realizability">realizability</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/computability">computability</a></strong></p> <p><a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a></p> <p><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>, <a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>, <a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></p> <h3 id="constructive_mathematics">Constructive mathematics</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a>, <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-topos">homotopy topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/canonical+form">canonical form</a>, <a class="existingWikiWord" href="/nlab/show/univalence">univalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>, <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable equality</a>, <a class="existingWikiWord" href="/nlab/show/decidable+subset">decidable subset</a>, <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited set</a>, <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></p> </li> </ul> <h3 id="realizability">Realizability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+topos">realizability topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+model">realizability model</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+interpretation">realizability interpretation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kleene%27s+first+algebra">Kleene's first algebra</a>, <a class="existingWikiWord" href="/nlab/show/Kleene%27s+second+algebra">Kleene's second algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/function+realizability">function realizability</a></p> </li> </ul> <h3 id="computability">Computability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/computability">computability</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computation">computation</a>, <a class="existingWikiWord" href="/nlab/show/computational+type+theory">computational type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function">computable function</a>, <a class="existingWikiWord" href="/nlab/show/partial+recursive+function">partial recursive function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+analysis">computable analysis</a>, <a class="existingWikiWord" href="/nlab/show/constructive+analysis">constructive analysis</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Type+Two+Theory+of+Effectivity">Type Two Theory of Effectivity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function+%28analysis%29">computable function (analysis)</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/exact+real+computer+arithmetic">exact real computer arithmetic</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+set">computable set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/persistent+homology">persistent homology</a>, <a class="existingWikiWord" href="/nlab/show/effective+homology">effective homology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+physics">computable physics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Church-Turing+thesis">Church-Turing thesis</a></p> </li> </ul> </div></div> <h4 id="type_theory">Type theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a></strong> <a class="existingWikiWord" href="/nlab/show/metalanguage">metalanguage</a>, <a class="existingWikiWord" href="/nlab/show/practical+foundations">practical foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/judgement">judgement</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hypothetical+judgement">hypothetical judgement</a>, <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/antecedents">antecedents</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\vdash</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/consequent">consequent</a>, <a class="existingWikiWord" href="/nlab/show/succedents">succedents</a></li> </ul> </li> </ul> <ol> <li><a class="existingWikiWord" href="/nlab/show/type+formation+rule">type formation rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+introduction+rule">term introduction rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+elimination+rule">term elimination rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/computation+rule">computation rule</a></li> </ol> <p><strong><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></strong> (<a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent</a>, <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional</a>, <a class="existingWikiWord" href="/nlab/show/observational+type+theory">observational type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>)</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/syntax">syntax</a></strong> <a class="existingWikiWord" href="/nlab/show/object+language">object language</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/theory">theory</a>, <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>/<a class="existingWikiWord" href="/nlab/show/type">type</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definition">definition</a>/<a class="existingWikiWord" href="/nlab/show/proof">proof</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a> (<a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/theorem">theorem</a></p> </li> </ul> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></strong> = <br /> <strong><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/programs+as+proofs">programs as proofs</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation type theory/category theory</a></strong></p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/logic">logic</a></th><th><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (<a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internal logic</a> of)</th><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object">object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/predicate">predicate</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/display+morphism">display morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof">proof</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/element">element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/generalized+element">generalized element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/term">term</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+rule">cut rule</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/composition">composition</a> of <a class="existingWikiWord" href="/nlab/show/classifying+morphisms">classifying morphisms</a> / <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> of <a class="existingWikiWord" href="/nlab/show/display+maps">display maps</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/introduction+rule">introduction rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/counit">counit</a> for hom-tensor adjunction</td><td style="text-align: left;">lambda</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/elimination+rule">elimination rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unit">unit</a> for hom-tensor adjunction</td><td style="text-align: left;">application</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+elimination">cut elimination</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">one of the <a class="existingWikiWord" href="/nlab/show/zigzag+identities">zigzag identities</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a></td></tr> <tr><td style="text-align: left;">identity elimination for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">the other <a class="existingWikiWord" href="/nlab/show/zigzag+identity">zigzag identity</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/eta+conversion">eta conversion</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/singleton">singleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated+object">(-2)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+0">h-level 0</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/false">false</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>, <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated+object">(-1)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product">product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product+type">product type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> (into <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> (into <a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (into <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> into <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> into <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> into <a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subterminal+objects">subterminal objects</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (of family of <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/bijection+set">bijection set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+of+isomorphisms">object of isomorphisms</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+type">equivalence type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+set">support set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+object">support object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a>/<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-image">n-image</a> of <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> into <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/n-truncation">n-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-truncation+modality">n-truncation modality</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/diagonal+function">diagonal function</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+relation">diagonal relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/path+space+object">path space object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>/<a class="existingWikiWord" href="/nlab/show/path+type">path type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/completely+presented+set">completely presented set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/discrete+object">discrete object</a>/<a class="existingWikiWord" href="/nlab/show/0-truncated+object">0-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+2">h-level 2</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/set">set</a>/<a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28infinity%2C1%29-category">internal 0-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>/<a class="existingWikiWord" href="/nlab/show/setoid">setoid</a> with its <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a> an actual <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+class">equivalence class</a>/<a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient">quotient</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>, <a class="existingWikiWord" href="/nlab/show/W-type">W-type</a>, <a class="existingWikiWord" href="/nlab/show/M-type">M-type</a></td></tr> <tr><td style="text-align: left;">higher <a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a></td></tr> <tr><td style="text-align: left;">-</td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+inductive+type">quotient inductive type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinduction">coinduction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/limit">limit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/preset">preset</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a> without <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universe">universe</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modality">modality</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/closure+operator">closure operator</a>, (<a class="existingWikiWord" href="/nlab/show/idempotent+monad">idempotent</a>) <a class="existingWikiWord" href="/nlab/show/monad">monad</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>, <a class="existingWikiWord" href="/nlab/show/monad+%28in+computer+science%29">monad (in computer science)</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;">(<a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed</a>) <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>/<a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof+net">proof net</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quantum+circuit">quantum circuit</a></td></tr> <tr><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a></td><td style="text-align: left;"></td><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">no-cloning theorem</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/synthetic+mathematics">synthetic mathematics</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+specific+embedded+programming+language">domain specific embedded programming language</a></td></tr> </tbody></table> </div> <p><strong><a class="existingWikiWord" href="/nlab/show/homotopy+levels">homotopy levels</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-type+theory">2-type theory</a>, <a class="existingWikiWord" href="/michaelshulman/show/2-categorical+logic">2-categorical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory+-+contents">homotopy type theory - contents</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a>, <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>, <a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+homotopy+type+theory">directed homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/HoTT+methods+for+homotopy+theorists">HoTT methods for homotopy theorists</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/semantics">semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/display+map">display map</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+a+topos">internal logic of a topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Mitchell-Benabou+language">Mitchell-Benabou language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kripke-Joyal+semantics">Kripke-Joyal semantics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type-theoretic+model+category">type-theoretic model category</a></li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/type+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#examples'>Examples</a></li> <li><a href='#references'>References</a></li> <ul> <li><a href='#general'>General</a></li> <li><a href='#CouplingProofAssistantsWithMachineLearningReferences'>Coupling proof assistants with machine learning</a></li> </ul> </ul> </div> <h2 id="idea">Idea</h2> <p>A <em>proof assistant</em> or <em>proof management system</em> is a kind of software designed to help with <a class="existingWikiWord" href="/nlab/show/proofs">proofs</a> in formalized <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a>. Many proof assistants resemble and/or include a <a class="existingWikiWord" href="/nlab/show/programming+language">programming language</a>.</p> <p>There are arguably two threads of current development in proof systems, which may be called “foundational” and “coverage”.</p> <p>The “foundational” work tries to find the best foundational theory to formalize mathematics (see also at <em><a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a></em>). Out of that work first came <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent types</a> (<a class="existingWikiWord" href="/nlab/show/Automath">Automath</a>, in the late 60s), then the <a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a> (early <a class="existingWikiWord" href="/nlab/show/Coq">Coq</a>), and the <a class="existingWikiWord" href="/nlab/show/calculus+of+inductive+constructions">calculus of inductive constructions</a> (current <a class="existingWikiWord" href="/nlab/show/Coq">Coq</a>). More recently a new wave of such work is being done in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> as another step in this direction. Coq’s library is not that large, except in the area of <a class="existingWikiWord" href="/nlab/show/group+theory">group theory</a> where the results of the work on <a class="existingWikiWord" href="/nlab/show/Feit-Thompson+theorem">Feit-Thompson theorem</a> has produced something larger.</p> <p>The “coverage” work tries to formalize as much as possible of mathematics in existing theories. For instance, for decades people have been building <a class="existingWikiWord" href="/nlab/show/Mizar">Mizar</a>‘s library (Mizar is based on <a class="existingWikiWord" href="/nlab/show/Tarski%E2%80%93Grothendieck+set+theory">Tarski–Grothendieck set theory</a> rather than <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>). Its library is a couple of orders of magnitude larger than anyone else’s. On the other hand, despite this quantity, it remains an issue to attack problems of contemporary research interest in these systems, see also at <em><a href="Mizar#ProblemOfPertinence">Mizar – problem of pertinence</a></em>.</p> <p>Similar to Mizar is <a class="existingWikiWord" href="/nlab/show/NuPRL">NuPRL</a>, <a class="existingWikiWord" href="/nlab/show/HOL+light">HOL light</a> and <a class="existingWikiWord" href="/nlab/show/Isabelle">Isabelle</a>, which all have decently sized libraries. (Isabelle can be used with either <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a>, like Mizar, or <a class="existingWikiWord" href="/nlab/show/higher-order+type+theory">higher-order type theory</a>, like the others.)</p> <h2 id="examples">Examples</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/proof+assistants">proof assistants</a>:</strong></p> <p>based on plain <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>/<a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Metamath">Metamath</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Mizar">Mizar</a>, <a class="existingWikiWord" href="/nlab/show/NuPRL">NuPRL</a>, <a class="existingWikiWord" href="/nlab/show/Isabelle">Isabelle</a>, <a class="existingWikiWord" href="/nlab/show/HOL">HOL</a></p> </li> </ul> <p>based on <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>/<a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Coq">Coq</a>, <a class="existingWikiWord" href="/nlab/show/Agda">Agda</a>, <a class="existingWikiWord" href="/nlab/show/Lean">Lean</a>, <a class="existingWikiWord" href="/nlab/show/Arend">Arend</a></li> </ul> <p id="BasedOnCubicalTypeTheory"> based on <a class="existingWikiWord" href="/nlab/show/cubical+type+theory">cubical type theory</a>:</p> <ul> <li> <p><a href="https://github.com/mortberg/cubicaltt">cubicaltt</a></p> </li> <li> <p><a href="http://github.com/redprl/redtt">redtt</a></p> </li> <li> <p><a href="http://github.com/mortberg/yacctt">yacctt</a></p> </li> <li> <p><a href="http://www.redprl.org/en/latest/">RedPRL</a></p> </li> <li> <p><a href="Agda#CubicalAgda">Cubical Agda</a></p> <ul> <li> <p><a href="https://github.com/agda/cubical">library and demos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/1lab">1lab</a> (cross-linked reference resource)</p> </li> </ul> </li> </ul> <p>based on <a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Agda-flat">Agda-flat</a>: <a href="http://www.cl.cam.ac.uk/~amp12/agda/internal-universes/code/agda-flat/install.txt">installation instructions</a></li> </ul> <p>based on <a class="existingWikiWord" href="/nlab/show/simplicial+type+theory">simplicial type theory</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Rzk">Rzk</a></li> </ul> <p>For <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal</a> <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/DisCoPy">DisCoPy</a></li> </ul> <p>For <a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a>:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/opetopic+type+theory">opetopic type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Globular">Globular</a>, <a class="existingWikiWord" href="/nlab/show/homotopy.io">homotopy.io</a></p> </li> </ul> <p><strong>projects for <a class="existingWikiWord" href="/nlab/show/formal+proof">formalization</a> of <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> with proof assistants:</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Archive+of+Formal+Proofs">Archive of Formal Proofs</a> (using <a class="existingWikiWord" href="/nlab/show/Isabelle">Isabelle</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ForMath+project">ForMath project</a> (using <a class="existingWikiWord" href="/nlab/show/Coq">Coq</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/MathScheme">MathScheme</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/UniMath+project">UniMath project</a> (using <a class="existingWikiWord" href="/nlab/show/Coq">Coq</a> and <a class="existingWikiWord" href="/nlab/show/Agda">Agda</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Xena+project">Xena project</a> (using <a class="existingWikiWord" href="/nlab/show/Lean">Lean</a>)</p> </li> </ul> <p>Other proof assistants</p> <ul> <li><a href="http://www.andromeda-prover.org/">Andromeda</a></li> </ul> <p>Historical projects that died out:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/The+QED+Project">The QED Project</a></li> </ul> </div> <h2 id="references">References</h2> <h3 id="general">General</h3> <p>Gentle exposition:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Th%C3%A9o+Winterhalter">Théo Winterhalter</a>, §1 of: <em>Formalisation and Meta-Theory of Type Theory</em>, Nantes (2020) [<a href="https://github.com/TheoWinterhalter/phd-thesis/releases/download/v1.2.1/TheoWinterhalter-PhD-v1.2.1.pdf">pdf</a>, <a href="https://github.com/TheoWinterhalter/phd-thesis">github</a>]</li> </ul> <p>Further exposition:</p> <ul> <li id="Avigad12"><a class="existingWikiWord" href="/nlab/show/Jeremy+Avigad">Jeremy Avigad</a>, <em>Interactive Theorem Proving, Automated Reasoning, and Mathematical Computation</em>, (2012) <a href="http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf">pdf slides</a></li> </ul> <p>On computer assisted proofs in <a class="existingWikiWord" href="/nlab/show/analysis">analysis</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Oscar+E.+Lanford">Oscar E. Lanford</a>, <em>Computer assisted proofs</em>, in: <em>Computational Methods in Field Theory</em>, Lecture Notes in Physics, <strong>409</strong>, Springer (1992) [<a href="https://doi.org/10.1007/3-540-55997-3_30">doi:10.1007/3-540-55997-3_30</a>]</li> </ul> <p>See also:</p> <ul> <li>Wikipedia, <em><a href="https://en.wikipedia.org/wiki/Proof_assistant">Proof assistant</a></em></li> </ul> <p>List of web resources:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Freek+Wiedijk">Freek Wiedijk</a>, <em>Digital math by alphabet</em> (<a href="http://www.cs.ru.nl/~freek/digimath/index.html">web</a>)</li> </ul> <p>See also</p> <ul> <li> <p><em><a href="http://www.cicm-conference.org/">Conference Series on Intelligent Computer Mathematics</a></em></p> <p>(<a href="http://cicm-conference.org/2014/cicm.php">2014</a>)</p> </li> <li> <p>Conference series on Interactive theorem proving</p> <p>(<a href="http://www.cs.uwyo.edu/~ruben/itp-2014/">2014</a>)</p> </li> </ul> <p>Parts of the above text are taken from <a href="http://mathoverflow.net/questions/133572/at-which-level-is-it-currently-possible-to-write-formal-proofs/134009#134009">this MO comment</a> by <a class="existingWikiWord" href="/nlab/show/Jacques+Carette">Jacques Carette</a>.</p> <p>Proof assistants specifically for <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>:</p> <ul> <li><a href="https://ncatlab.org/homotopytypetheory/show/HomePage">HoTT wiki</a>, <em><a class="existingWikiWord" href="/homotopytypetheory/show/Proof+Assistants">Proof Assistants</a></em></li> </ul> <p>See also</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Kevin+Buzzard">Kevin Buzzard</a>, <em><a href="https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/">Xena project</a></em></p> <p>on <a class="existingWikiWord" href="/nlab/show/formal+proof">formal proof</a> and proof assistants in undergraduate mathematics.</p> </li> </ul> <div> <h3 id="CouplingProofAssistantsWithMachineLearningReferences">Coupling proof assistants with machine learning</h3> <p>On coupling <a class="existingWikiWord" href="/nlab/show/proof+assistants">proof assistants</a> with <a class="existingWikiWord" href="/nlab/show/machine+learning">machine learning</a>:</p> <ul> <li> <p>Li-An Yang et al, <em>Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants</em> [<a href="https://arxiv.org/abs/1602.07455">arXiv:1602.07455</a>]</p> </li> <li> <p>Klaus Mainzer: <em>From Proof Theory to Proof Assistants – Challenges of Responsible Software and AI</em>, talk at <em>Arbeitstagung Bern-München</em> (2019) [<a href="https://cj-xu.github.io/abm19/mainzer.pdf">pdf</a>]</p> </li> <li> <p>Kaiyu Yang, Jia Deng: <em>Learning to Prove Theorems via Interacting with Proof Assistants</em> [<a href="https://arxiv.org/abs/1905.09381">arXiv:1905.09381</a>]</p> </li> <li> <p>Cezary Kaliszyk: <em><a href="http://cl-informatik.uibk.ac.at/teaching/ws23/mltp/overview.php">Machine Learning for Theorem Proving</a></em>, lecture notes (2023) [pdf:<a href="http://cl-informatik.uibk.ac.at/teaching/ws23/mltp/01.pdf">1</a>, <a href="http://cl-informatik.uibk.ac.at/teaching/ws23/mltp/02.pdf">2</a>, <a href="http://cl-informatik.uibk.ac.at/teaching/ws23/mltp/03.pdf">3</a>, <a href="http://cl-informatik.uibk.ac.at/teaching/ws23/mltp/04.pdf">4</a>, <a href="http://cl-informatik.uibk.ac.at/teaching/ws23/mltp/05.pdf">5</a>, <a href="http://cl-informatik.uibk.ac.at/teaching/ws23/mltp/06.pdf">6</a>]</p> </li> <li> <p>Garrett Mills: <em><a href="https://glmdev.medium.com/adventures-in-ai-assisted-proof-generation-dc946597503a">Adventures in AI-assisted proof generation</a></em> (Mar 2023)</p> </li> <li> <p><a href="https://neurips.cc/Conferences/2023">NeurIPS 2023</a>: <em><a href="https://machine-learning-for-theorem-proving.github.io/">Tutorial on Machine Learning for Theorem Proving</a></em> (2023)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Terence+Tao">Terence Tao</a>: <em>Machine-Assisted Proof</em>, Notices of the AMS <strong>72</strong> 1 (2024) [<a href="https://doi.org/10.1090/noti3041">doi:10.1090/noti3041</a>, <a href="https://www.ams.org/journals/notices/202501/rnoti-p6.pdf">pdf</a>, full issue:<a href="https://www.ams.org/notices/202501/202501FullIssue.pdf">pdf</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Terence+Tao">Terence Tao</a>: <em>Machine-Assisted Proof</em>, AMS Colloquium Lectures at the 2024 Joint Mathematics Meetings [video:<a href="https://youtu.be/AayZuuDDKP0">YT</a>]</p> </li> <li> <p>Peiyang Song, Kaiyu Yang, Anima Anandkumar: <em>Towards Large Language Models as Copilots for Theorem Proving in Lean</em> [<a href="https://arxiv.org/abs/2404.12534">arXiv:2404.12534</a>]</p> </li> <li> <p>Leni Aniva et al.: <em>Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4</em> [<a href="https://arxiv.org/abs/2410.16429">arXiv:2410.16429</a>]</p> </li> <li> <p>Kaiyu Yang et al.: <em>Formal Mathematical Reasoning: A New Frontier in AI</em> [<a href="https://arxiv.org/abs/2412.16075">arXiv:2412.16075</a>]</p> </li> </ul> </div></body></html> </div> <div class="revisedby"> <p> Last revised on March 17, 2025 at 19:08:02. See the <a href="/nlab/history/proof+assistant" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/proof+assistant" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/5013/#Item_14">Discuss</a><span class="backintime"><a href="/nlab/revision/proof+assistant/30" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/proof+assistant" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/proof+assistant" accesskey="S" class="navlink" id="history" rel="nofollow">History (30 revisions)</a> <a href="/nlab/show/proof+assistant/cite" style="color: black">Cite</a> <a href="/nlab/print/proof+assistant" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/proof+assistant" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>