Comment by aldanor

I've formalised a few dozen papers from 80s-90s with lean and holy cow the number of author's typos and straight up errors and sometimes false statements is pretty scary. The solution path may not be the one indicated or used by the author, but at least you can easily spot all those issues which would have been very hard to do by hand