问题标签 [mizar]

我想用我能想到的Mizar数学定理证明器语言编写最简单的证明。所以我想到了以下几点：

存在 x \in Nat : x = 1

没有什么比我能想到的更简单的了。我给了它以下尝试：

但正如你所见，Mizar 不喜欢我的证明。我错过了什么？

这仍然不起作用：

如果这不是此类问题的正确堆栈交换站点，请让我知道哪里更合适。也让我知道这个问题是否有更好的标签，我会添加它们（或者如果你想要/可以，自己添加它们）。如果相关的话，我也在Mac上。

我正在尝试使用 mizar。我已经下载了它，现在正在尝试遵循本教程：https ://www.cs.ru.nl/~freek/mizar/mizman.ps.gz （您可以通过谷歌搜索“在中编写 Mizar 文章”在线找到本教程九个简单的步骤'并按照第一个链接）。

我正在尝试按照第 3 页（页面中上部）教程推荐的命令 mizf text/my_mizar.miz。问题似乎是我缺少一个名为 mml.ini 的文件，我不确定将这个文件放在哪里。

我已经尝试将它放在顶层目录中（例如，在 / 中），但这不起作用（它还要求我 sudo 到 root，而我不想这样做）。这是我的控制台的副本，让您了解我所做的事情。