Hacker News Reader

Comment by cs_throwaway | Hacker News Reader

There is no nice way to tell someone that you’ve scooped them, and this is industrial scale scooping.

A few papers have been retracted, but it looks like many are withstanding intense scrutiny. Lean is making the results more likely to be correct, but I think making them harder to understand.

The world has changed and you’ll know a math department is making a serious attempt to adapt when it teaches a required Lean course in freshman year.

View on HN

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.

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