Isabelle (proof assistant)

Example proof

Isabelle allows proofs to be written in two different styles, the procedural and the declarative. Procedural proofs specify a series of tactics (theorem proving functions/procedures) to apply. While reflecting the procedure that a human mathematician might apply to proving a result, they are typically hard to read as they do not describe the outcome of these steps. This style is "considered harmful" in the Isabelle documentation.

On the other hand, declarative proofs (supported by Isabelle's proof language, Isar) specify the actual mathematical operations to be performed, and are therefore more easily read and checked by humans.

For example, a declarative proof by contradiction in Isar that the square root of two is not rational can be written as follows.

<style data-mw-deduplicate="TemplateStyles:r1239334494" typeof="mw:Extension/templatestyles mw:Transclusion" about="#mwt31" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"theorem"}},"i":0}}]}' id="mwbw">@media screen{html.skin-theme-clientpref-night .mw-parser-output div:not(.notheme)>.tmp-color,html.skin-theme-clientpref-night .mw-parser-output p>.tmp-color,html.skin-theme-clientpref-night .mw-parser-output table:not(.notheme) .tmp-color{color:inherit!important}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output div:not(.notheme)>.tmp-color,html.skin-theme-clientpref-os .mw-parser-output p>.tmp-color,html.skin-theme-clientpref-os .mw-parser-output table:not(.notheme) .tmp-color{color:inherit!important}}</style><span class="tmp-color" style="color:darkblue" about="#mwt31" id="mwcA">theorem</span> sqrt2_not_rational: <span style="color:olive" about="#mwt33" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"sqrt 2 ∉ {{mathbb|Q}}\""}},"i":0}}]}' id="mwcQ">"sqrt 2 ∉ ℚ"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt34" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"proof"}},"i":0}}]}' id="mwcg"/><span class="tmp-color" style="color:darkblue" about="#mwt34" id="mwcw">proof</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt36" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"let"}},"i":0}}]}' id="mwdA"/><span class="tmp-color" style="color:darkblue" about="#mwt36" id="mwdQ">let</span> ?x = <span style="color:olive" about="#mwt38" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"sqrt 2\""}},"i":0}}]}' id="mwdg">"sqrt 2"</span> <span style="color:blue" about="#mwt39" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"blue","href":"./Template:Blue"},"params":{"1":{"wt":"assume"}},"i":0}}]}' id="mwdw">assume</span> <span style="color:olive" about="#mwt40" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"?x ∈ {{mathbb|Q}}\""}},"i":0}}]}' id="mweA">"?x ∈ ℚ"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt41" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"then"}},"i":0}}]}' id="mweQ"/><span class="tmp-color" style="color:darkblue" about="#mwt41" id="mweg">then</span> <span style="color:blue" about="#mwt43" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"blue","href":"./Template:Blue"},"params":{"1":{"wt":"obtain"}},"i":0}}]}' id="mwew">obtain</span> m n :: nat <span style="color:green;" about="#mwt44" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"green","href":"./Template:Green"},"params":{"1":{"wt":"where"}},"i":0}}]}' id="mwfA">where</span> sqrt_rat: <span style="color:olive" about="#mwt45" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"¦?x¦ {{=}} m / n\""}},"i":0}}]}' id="mwfQ">"¦?x¦ = m / n"</span> <span style="color:green;" about="#mwt46" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"green","href":"./Template:Green"},"params":{"1":{"wt":"and"}},"i":0}}]}' id="mwfg">and</span> lowest_terms: <span style="color:olive" about="#mwt47" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"coprime m n\""}},"i":0}}]}' id="mwfw">"coprime m n"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt48" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwgA"/><span class="tmp-color" style="color:darkblue" about="#mwt48" id="mwgQ">by</span> (rule Rats_abs_nat_div_natE) <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt50" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"hence"}},"i":0}}]}' id="mwgg"/><span class="tmp-color" style="color:darkblue" about="#mwt50" id="mwgw">hence</span> <span style="color:olive" about="#mwt52" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"m^2 {{=}} ?x^2 * n^2\""}},"i":0}}]}' id="mwhA">"m^2 = ?x^2 * n^2"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt53" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwhQ"/><span class="tmp-color" style="color:darkblue" about="#mwt53" id="mwhg">by</span> (auto simp add: power2_eq_square) <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt55" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"hence"}},"i":0}}]}' id="mwhw"/><span class="tmp-color" style="color:darkblue" about="#mwt55" id="mwiA">hence</span> eq: <span style="color:olive" about="#mwt57" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"m^2 {{=}} 2 * n^2\""}},"i":0}}]}' id="mwiQ">"m^2 = 2 * n^2"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt58" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"using"}},"i":0}}]}' id="mwig"/><span class="tmp-color" style="color:darkblue" about="#mwt58" id="mwiw">using</span> of_nat_eq_iff power2_eq_square <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt60" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwjA"/><span class="tmp-color" style="color:darkblue" about="#mwt60" id="mwjQ">by</span> fastforce <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt62" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"hence"}},"i":0}}]}' id="mwjg"/><span class="tmp-color" style="color:darkblue" about="#mwt62" id="mwjw">hence</span> <span style="color:olive" about="#mwt64" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"2 dvd m^2\""}},"i":0}}]}' id="mwkA">"2 dvd m^2"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt65" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwkQ"/><span class="tmp-color" style="color:darkblue" about="#mwt65" id="mwkg">by</span> simp <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt67" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"hence"}},"i":0}}]}' id="mwkw"/><span class="tmp-color" style="color:darkblue" about="#mwt67" id="mwlA">hence</span> <span style="color:olive" about="#mwt69" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"2 dvd m\""}},"i":0}}]}' id="mwlQ">"2 dvd m"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt70" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwlg"/><span class="tmp-color" style="color:darkblue" about="#mwt70" id="mwlw">by</span> simp <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt72" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"have"}},"i":0}}]}' id="mwmA"/><span class="tmp-color" style="color:darkblue" about="#mwt72" id="mwmQ">have</span> <span style="color:olive" about="#mwt74" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"2 dvd n\""}},"i":0}}]}' id="mwmg">"2 dvd n"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt75" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"proof"}},"i":0}}]}' id="mwmw"/><span class="tmp-color" style="color:darkblue" about="#mwt75" id="mwnA">proof</span> - <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt77" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"from"}},"i":0}}]}' id="mwnQ"/><span class="tmp-color" style="color:darkblue" about="#mwt77" id="mwng">from</span> <span style="color:olive" about="#mwt79" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"‹2 dvd m›"}},"i":0}}]}' id="mwnw">‹2 dvd m›</span> <span style="color:blue" about="#mwt80" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"blue","href":"./Template:Blue"},"params":{"1":{"wt":"obtain"}},"i":0}}]}' id="mwoA">obtain</span> k <span style="color:green;" about="#mwt81" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"green","href":"./Template:Green"},"params":{"1":{"wt":"where"}},"i":0}}]}' id="mwoQ">where</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt82" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"olive"},"2":{"wt":"\"m {{=}} 2 * k\""}},"i":0}}]}' id="mwog"/><span class="tmp-color" style="color:olive" about="#mwt82" id="mwow">"m = 2 * k"</span> ..<!--The two dots refer to a complete proof of this claim--> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt84" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"with"}},"i":0}}]}' id="mwpA"/><span class="tmp-color" style="color:darkblue" about="#mwt84" id="mwpQ">with</span> eq <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt86" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"have"}},"i":0}}]}' id="mwpg"/><span class="tmp-color" style="color:darkblue" about="#mwt86" id="mwpw">have</span> <span style="color:olive" about="#mwt88" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"2 * n^2 {{=}} 2^2 * k^2\""}},"i":0}}]}' id="mwqA">"2 * n^2 = 2^2 * k^2"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt89" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwqQ"/><span class="tmp-color" style="color:darkblue" about="#mwt89" id="mwqg">by</span> simp <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt91" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"hence"}},"i":0}}]}' id="mwqw"/><span class="tmp-color" style="color:darkblue" about="#mwt91" id="mwrA">hence</span> <span style="color:olive" about="#mwt93" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"2 dvd n^2\""}},"i":0}}]}' id="mwrQ">"2 dvd n^2"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt94" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwrg"/><span class="tmp-color" style="color:darkblue" about="#mwt94" id="mwrw">by</span> simp <span style="color:blue" about="#mwt96" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"blue","href":"./Template:Blue"},"params":{"1":{"wt":"thus"}},"i":0}}]}' id="mwsA">thus</span> <span style="color:olive" about="#mwt97" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"2 dvd n\""}},"i":0}}]}' id="mwsQ">"2 dvd n"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt98" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwsg"/><span class="tmp-color" style="color:darkblue" about="#mwt98" id="mwsw">by</span> simp <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt100" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"qed"}},"i":0}}]}' id="mwtA"/><span class="tmp-color" style="color:darkblue" about="#mwt100" id="mwtQ">qed</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt102" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"with"}},"i":0}}]}' id="mwtg"/><span class="tmp-color" style="color:darkblue" about="#mwt102" id="mwtw">with</span> <span style="color:olive" about="#mwt104" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"‹2 dvd m›"}},"i":0}}]}' id="mwuA">‹2 dvd m›</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt105" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"have"}},"i":0}}]}' id="mwuQ"/><span class="tmp-color" style="color:darkblue" about="#mwt105" id="mwug">have</span> <span style="color:olive" about="#mwt107" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"2 dvd gcd m n\""}},"i":0}}]}' id="mwuw">"2 dvd gcd m n"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt108" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwvA"/><span class="tmp-color" style="color:darkblue" about="#mwt108" id="mwvQ">by</span> (rule gcd_greatest) <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt110" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"with"}},"i":0}}]}' id="mwvg"/><span class="tmp-color" style="color:darkblue" about="#mwt110" id="mwvw">with</span> lowest_terms <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt112" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"have"}},"i":0}}]}' id="mwwA"/><span class="tmp-color" style="color:darkblue" about="#mwt112" id="mwwQ">have</span> <span style="color:olive" about="#mwt114" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"olive","href":"./Template:Olive"},"params":{"1":{"wt":"\"2 dvd 1\""}},"i":0}}]}' id="mwwg">"2 dvd 1"</span> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt115" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwww"/><span class="tmp-color" style="color:darkblue" about="#mwt115" id="mwxA">by</span> simp <span style="color:blue" about="#mwt117" typeof="mw:Transclusion" data-mw='{"parts":[{"template":{"target":{"wt":"blue","href":"./Template:Blue"},"params":{"1":{"wt":"thus"}},"i":0}}]}' id="mwxQ">thus</span> False <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt118" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"using"}},"i":0}}]}' id="mwxg"/><span class="tmp-color" style="color:darkblue" about="#mwt118" id="mwxw">using</span> odd_one <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt120" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"by"}},"i":0}}]}' id="mwyA"/><span class="tmp-color" style="color:darkblue" about="#mwt120" id="mwyQ">by</span> blast <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494" about="#mwt122" typeof="mw:Extension/templatestyles mw:Transclusion" data-mw='{"name":"templatestyles","attrs":{"src":"Template:Color/styles.css"},"parts":[{"template":{"target":{"wt":"color","href":"./Template:Color"},"params":{"1":{"wt":"darkblue"},"2":{"wt":"qed"}},"i":0}}]}' id="mwyg"/><span class="tmp-color" style="color:darkblue" about="#mwt122" id="mwyw">qed</span>

Applications

Isabelle has been used to aid formal methods for the specification, development and verification of software and hardware systems.

Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. Many of the formal proofs are, as mentioned, maintained in the Archive of Formal Proofs, which contains (as of 2019) at least 500 articles with over 2 million lines of proof in total.

• In 2009, the L4.verified project at NICTA produced the first formal proof of functional correctness of a general-purpose operating system kernel: the seL4 (secure embedded L4) microkernel. The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script to verify 7,500 lines of C. The verification covers code, design, and implementation, and the main theorem states that the C code correctly implements the formal specification of the kernel. The proof uncovered 144 bugs in an early version of the C code of the seL4 kernel, and about 150 issues in each of design and specification.

• The definition of the programming language Lightweight Java was proven type-sound in Isabelle.

Alternatives

Several languages and systems provide similar functions:

• Agda, written in Haskell
• Rocq (formerly named Coq), written in OCaml
• Lean, written in Lean and C++
• LEGO, written in Standard ML of New Jersey
• Mizar system, written in Free Pascal
• Metamath, written in ANSI C
• Prover9, written in C, with a GUI written in Python
• Twelf, written in Standard ML