I accidentally proved 2=3

Stream: new members

[Mr Proof]

How can I detect fallacious proofs like this:

variable (a:2=3)

theorem proof:(2=3):=a
/- Q E D -/

[Mauricio Collares]

#print proof

[Vincent Beffara]

It's not fallacious, it just has type 2 = 3 → 2 = 3

[Markus Schmaus]

You proved 2 = 3 → 2 = 3, there is nothing wrong with that.

variable (a:2=3)

theorem proof : (2=3):=a
/- Q E D -/

#check proof -- proof (a : 2 = 3) : 2 = 3

[Vincent Beffara]

More to the point: this goes to show that it is safer to avoid variables in Prop

[Mr Proof]

Is there a way to check if a proof has used variables by mistake? e.g. if someone had define variable (proof2equals3:2=3) in another library

[Johan Commelin]

variable is local to your file (or section)

[Kyle Miller]

In addition to Mauricio's suggestion, you can hover over proof in VS Code and see its type.

[Mark Fischer]

A proof, but you can see that you've relied on an extra axiom:

axiom a : 2 = 3

theorem proof : 2 = 3 := a
/- Q E D -/

#check proof          -- proof : 2 = 3
#print axioms proof   -- 'proof' depends on axioms: [a]