No.10998918 ViewReplyOriginalReport
Can a trusting trust attack be used to trick mathematicians into accepting false proofs?

http://wiki.c2.com/?TheKenThompsonHack

We modify the theorem prover and compiler in order to make the theorem prover pass false theorems.
Looking at the source of the theorem prover shews nothing abnormal. The compiler inserts the bug when compiling the theorem prover. Moreover, the compiler inserts this bug into the compiler when compiling itself. Inspecting the compiler source reveals nothing you can even use the theorem prover to prove the correctness of the compiler and of itself.