Hacker News Reader

would Wiles be willing to transcribe his proof for the metamath verifier? it can be done offline indeed...

I asked about Wiles, because others frequently run into issues while formalizing.