Formalize another proof of Fermat's two-squares theorem using corner …

…shapes rather than windmills.
HOL-Theorem-Prover · Aug 12, 2023 · d020bcf · d020bcf
1 parent f24365d
commit d020bcf
Show file tree

Hide file tree

Showing 3 changed files with 1,082 additions and 0 deletions.
diff --git a/examples/fermat/twosq/README.md b/examples/fermat/twosq/README.md
@@ -16,3 +16,4 @@ These theories support the formalisation of an algorithm for Fermat's Two Square
 * __windmill__, definitions of windmill, mill, flip, and zagier.
 * __twoSquares__, existence, uniqueness and algorithm of two squares theorem.
 * __quarity__, zig and zag, tik and tok, mill structure, and search for two squares.
+* __corner__, an adaptation of a partition proof using corner pieces.