> And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. I am not so sure

> And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. I am not so sure about this, actually. "twisted type theory" looks like type theory more in the original Bertrand Russel sense than in the modern (Martin Loef, Jean-Yves Girard, etc.) sense.