Mizar を用いた動的検証可能な数学ドキュメンテーション https://mizar.work/dokuwiki/ Thu, 30 Apr 2026 20:30:23 +0000 FeedCreator 1.8 https://mizar.work/dokuwiki/lib/exe/fetch.php?media=wiki:dokuwiki.svg https://mizar.work/dokuwiki/ https://mizar.work/dokuwiki/doku.php?id=example&rev=1748500509 第1章 TARSKIの公理系 このテキストは集合論を題材に mizar を使った数学定理の記述が実際にどのようになされているかを説明します。 mizar では，その数学記述言語によって書かれたテキストを \(x, y, z, u, N, M, X, Y, Z\)\[ ((\forall x)(x \in X \Leftrightarrow x \in Y)) \Rightarrow X=Y \]\(x\)\(x \in X \Leftrightarrow x \in Y\)\(X\)\(Y\)\(X = Y\)\(x\)\(\{x\}\)\(x\)\(y\)\(\{x, y\}\)\(y\)\(\{y\}\)\(x\)\[ x \in \{y\} \Leftrightarrow x = y \]\(y\)\(z\)\(\{y, z\}\)\(x\)\[ x \in \{y, z\} \Leftrightarrow x = y \lor x = z \]\[ \{y, z\} = \{z, y\} \]\(X\)\(Y\)\(X\)\(Y\)\(X\)\(Y\)\(X \subsete… anonymous@undisclosed.example.com (Anonymous) Thu, 29 May 2025 06:35:09 +0000 https://mizar.work/dokuwiki/doku.php?id=sidebar&rev=1744083504 ---------- * 基本文法と動作 * 体験デモ * Mizar Verifiable Docs (日本語) * GitHub リポジトリ * note クリエイターページ anonymous@undisclosed.example.com (Anonymous) Tue, 08 Apr 2025 03:38:24 +0000 https://mizar.work/dokuwiki/doku.php?id=start&rev=1744336091 パート1 ここには通常の内容（説明文など）が入ります。 パート2 こちらも通常の内容です。 anonymous@undisclosed.example.com (Anonymous) Fri, 11 Apr 2025 01:48:11 +0000