There's a proposed proof of abc conjecture that is supposedly more readable. Here is a discussion thread about it: https://www.reddit.com/r/math/comments/1bhiz

There's a proposed proof of abc conjecture that is supposedly more readable. Here is a discussion thread about it: https://www.reddit.com/r/math/comments/1bhiz0s/construction_of_arithmetic_teichmuller_spaces_iv/ https://www.reddit.com/r/math/comments/1bhiz0s/construction_... It would be nice if this one were formalized in Lean (or Coq or HOL) though.