alt Hacker NewsIMO the "forty hours per page" rule is not up to date, and more a consequence of lacking proof automation in 2005. From what I understand about Lean, this has been one of the things that they have put a lot of effort into improving, making proof mechanization more palatable to the mathematically inclined, as opposed to just logicians.
Replies
YetAnotherNick • today at 3:27 AM
Lean went other way on automation that there is no automation. Isabelle users frequently point that decades old isabelle is better than Lean on this. In the end Lean approach proved to be better with LLM as the outer loop is automation.
What is your estimate for the number of hours to formalize one page of undergraduate mathematics? Maybe you are saying this is close to zero, if/when Mathlib eventually covers all of undergraduate math?