`solution.lean` is a 12mb file
I looks like we are breezing past the point where unassisted humans can understand any of this
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.
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.
We pretty much crossed this bridge in 1976 with the proof of the four-color theorem: https://en.wikipedia.org/wiki/Four_Color_Theorem