Verification of Formal proofs

[sivakishoresk]

Many of the theorem statements does not have formal proofs(they have the sorry tags). If I have a generated proof for a theorem how should I evaluate it, even if we have a predicted proof and ground truth proof, how do I go for semantic evaluation between these two.
Someone please help me with this.

[DyeKuu]

Hi @sivakishoresk ! Yes you need a formal engine to check whether the generated one is correct or not. The lean version in this repo is Lean 3.
https://github.com/leanprover/lean3
https://leanprover-community.github.io/lean-web-editor/

The ground truth proof is not unique: any proof that passes the formal engine check is a valid and success proof. The theorem statements are there only to set up a goal.