In order to install Lean 3, follow the manual.
In order to download this project, run leanproject get madvorak/grammars in your Unix-like command line.
In order to check that the proofs are correct, run ./mk from the root directory of this project.
The script will output Result: SUCCESS if everything builds successfully.
Below you find what has been completed so far.
Non-closure under intersection (*)
Non-closure under complement (*)
* missing proof: Context-free pumping lemma
(a.k.a. general grammars, a.k.a. type-0 grammars, a.k.a. recursively-enumerable grammars, a.k.a. phrase-structure grammars, a.k.a. grammars)