It definitely poses a challenge to the question of what a mathematical proof actually is. One of the things about mathematics is in a way its 'obviousness', there's a way in which once something is proven its intelligble to mathematicians in an immediate, direct sense.

A 600 page proof that requires essentially a new branch of idiosyncratic mathematics which as an end result is barely understandable even by peers in the field almost moves it from mathematics into the realm of empirical science, where people are often for years occupied with interpretation of data and discussions about how significant a finding is.

As mathematics moves on to tackle more and more complicated questions I think it's interesting to ask if there will be a push back against complicated solutions, focus on simplicity as integral to solving a mathematical problem, and so on.

Massive hard to read code makes up 99% of software in the real world

Most programs are not correct. You'd have to refer to number of bugs.

Surely not the best example, but Terry A. Davis' (RIP) TempleOS was written in a very idiosyncratic style (he even invented his own programming language (HolyC) for this).

TempleOS is awesome

Being able to mix text, images, 3d models, etc in a terminal session is something that modern OSes still haven't gotten around to doing. Terry may have been crazy but he was right about a lot of things and unlike many, he had the skills to implement his ideas