Comment by ykonstant

I am not important enough to be receiving crackpot proofs, but if I ever do, I will enthusiastically suggest they formalize their work in Lean. Hmm, I wonder whether that would lead to crackpots making a fuss at the Zulip chat.