Just yesterday I started learning the Lean proof assistant. It seems that 
Metamath can verify proofs using a much simpler approach. What are the key 
differences?

Reply via email to