Semantic Analysis of Proofs

Stream: lean4

[Siva Gollapalli]

If I have 2 formal proofs for a same theorem with me, then how should I do the semantic evaluation or if I have a formal proof and theorem statement, could we verify that the proof is correct for the theorem statement ?

[Henrik Böving]

You write a theorem declaration followed by your proof? I don't quite see what you are getting at here, could you elaborate

[Siva Gollapalli]

Screenshot-2024-07-17-at-11.11.19AM.png

These are two different proofs for the same theorem right. Do we have a way to check if both proofs are correct

[Chris Bailey]

You try to tell Lean they're both proofs of the statement. You put the proofs on the right hand side of the := and see if Lean complains.

[Michael Rothgang]

By the way: it looks like you're using Lean 3 syntax. Have you considered switching to Lean 4? My impression is that you will get very few answers about Lean 3 here, as everybody has moved on and is slowly forgetting all the Lean 3 details...