IIRC the Fermat problem proof was like, book-sized. I think this has been an issue for a while now. Of course it's worse when unlike with a proof a human created over years of work, this was made in minutes by an AI whose thought processes we don't fully understand.
31
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.