 Using the design ideas implemented in Metamath, Raph Levien has implemented very small proof checker, "mmverify.py", at only 500 lines of Python code.Ghilbert is a similar though more elaborate language based on mmverify.py.Levien would like to implement a system where several people could collaborate and his work is emphasizing modularity and connection between small theories.