theorem-proving - 初学者，无法导入精益

Question

我是一个绝对的初学者，不是程序员，正在尝试使用 Logic and Proof 学习形式验证.我无法在精益中导入任何东西。

我将二进制文件的 tar 文件提取到 /tmp 然后执行

/tmp/lean-3.4.1-linux/bin/./lean /tmp/test.lean

除非我正在导入任何东西，否则它会起作用。所以如果我的文件 test.lean 只是说

open classical
example (P : Prop) : P ∨ ¬ P := em P

没有错误。但是，如果同一个文件改为显示

import data.set

我收到错误信息

/tmp/test.lean:1:0: error: file 'data/set' not found in the LEAN_PATH  
/tmp/test.lean:1:0: error: invalid import: data.set  
could not resolve import: data.set

import data.nat 会发生类似的错误。

我做错了什么，我该怎么办？我正在使用 Ubuntu 16.04。请注意，由于我是初学者，我从未从源代码编译过任何东西。

Answer 1

我通过直接联系 Avigad 教授找到了解决方案。

原来这本书不仅使用了标准库，还使用了精益数学组件库，mathlib .安装它对我有用。我现在可以执行 import data.set 而不会出错。