<- Back
Comments (16)
- black_knightI wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries.My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof! (Repost of a earlier comment, but I feel it fits better here)
- RantyDaveI love that “grind” is a keyword.
- abhvThis is a very impressive result. Bravo to that team.
- rawlingFront-page discussion: https://news.ycombinator.com/item?id=49568506
- ks2048Now we have what Fermat tried to write in the margin: aa2d8b34692b16c70f699536de0d8e75b9a3e9ef
- DoctorOetkerMine is much shorter though...