Mizar を用いた動的検証可能な数学ドキュメンテーション https://mizar.work/dokuwiki/ Thu, 30 Apr 2026 19:16:00 +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=en:example&rev=1744082392 Chapter 1 TARSKI's axiomatic system This text explains how the description of mathematical theorems is actually carried out using Mizar with set theory as the subject matter. In Mizar, texts written in its mathematical description language are called \(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… anonymous@undisclosed.example.com (Anonymous) Tue, 08 Apr 2025 03:19:52 +0000 https://mizar.work/dokuwiki/doku.php?id=en:sidebar&rev=1744083568 ---------- * Basic Syntax and Behavior * Interactive Demo * Mizar Verifiable Docs(English) * GitHub repository * note creator page anonymous@undisclosed.example.com (Anonymous) Tue, 08 Apr 2025 03:39:28 +0000 https://mizar.work/dokuwiki/doku.php?id=en:start&rev=1744010211 part 1 regular content part 2 regular content anonymous@undisclosed.example.com (Anonymous) Mon, 07 Apr 2025 07:16:51 +0000