logoalt Hacker News

VMGtoday at 10:39 AM3 repliesview on HN

`solution.lean` is a 12mb file

I looks like we are breezing past the point where unassisted humans can understand any of this


Replies

medlertoday at 12:28 PM

We pretty much crossed this bridge in 1976 with the proof of the four-color theorem: https://en.wikipedia.org/wiki/Four_Color_Theorem

show 1 reply
glimshetoday at 11:06 AM

I understand the spirit of what you're saying, but "unassisted humans" isn't a good yardstick. There's hardly anything "unassisted" humans understand today... We require plenty of assistance from computer tools in most scientific discoveries.

show 1 reply
hyperpapetoday at 11:34 AM

This is based on a 108 page prose paper that the repository links to. Of course, that's a very difficult paper as well, I don't know how many people would be qualified to read and digest it, but they do exist.