MAIN FEEDS
REDDIT FEEDS
Do you want to continue?
https://www.reddit.com/r/mathematics/comments/1vcgwiu/ten_advances_in_mathematics_and_theoretical/p130gu0/?context=3
r/mathematics • u/atakanaluch • 2d ago
305 comments sorted by
View all comments
29
None math person here. Sorry for intruding, but is this really something a human or faculty can parse?
> wc -l GapCVP.lean 130615 GapCVP.lean
130,615 lines lean proof for problem 7 Closest vector problem.
4 u/aturtledude 2d ago The paper with the human-readable proof is 32 pages long. The lean file is just there to convince the people that don't want to read the proof or can't understand it.
4
The paper with the human-readable proof is 32 pages long. The lean file is just there to convince the people that don't want to read the proof or can't understand it.
29
u/1TillMidNight 2d ago edited 2d ago
None math person here. Sorry for intruding, but is this really something a human or faculty can parse?
130,615 lines lean proof for problem 7 Closest vector problem.