The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

I am investigating fake proofs that look plausible to human forensics.

Why is it wrong to declare a proven theorem as an axiom? (this appears 
counter intuitive to me)

Theorem T : Prop.
exact False.
Defined.

Axiom A : T.

Lemma FUCKMS: False.
pose proof A. compute in H. contradiction.
Defined.

Coq < Print Assumptions FUCKMS.
Axioms:
A : T

If $T$ were False, how was it proven as a theorem?

Thank you.

-- 
joro