Return to Article Details A Mathematical Model of Automatic Verification of Formalized Proofs and a Conservative Presentation Interface over Lean Download Download PDF