Hacker News Reader

Why do you believe that learning Lean is a better use of time when the AI is clearly better at writing and interpreting Lean than it is writing quality papers? At this point, Lean is for autoformalization, no one is really supposed to read it.

View on HN

Well, you don't necessarily need to read the proof, but the proof is useless if you don't read the specification.

That's fair, but I would argue that reading the specification is very easy by comparison. A quick one hour tutorial is usually enough judging from my students' experiences.

The Lean proof to Fermat's Last Theorem is 13 mil lines.

The one for the quasi-Riemann Hypothesis is half a million.

Indeed! Almost none of these most math folks are likely to read. The only thing to read is the statement, which is only a handful of lines in both cases. The point of Lean is that if that statement compiles and is validated by hand to be equivalent to the natural language statement, then it is true. That was what I was trying to say here.

Reply on news.ycombinator.com