Comment by lacker

You would have to not use a type-based proof system. I think those are not going to be the "as simple as possible" ones. Consider metamath for example.