Fair points, but you are minimizing the important detail that mathematics is also a social activity, and so any argument about what constitutes mathematics shou

Fair points, but you are minimizing the important detail that mathematics is also a social activity, and so any argument about what constitutes mathematics should be viewed with that in mind. Mathematicians are interested in math because they want to understand things (meaning they can construct abstractions and develop logical lines of reasoning that fit within the limits of human cognition), so that they can develop new concepts and utilize existing ones in novel ways. Using a computer to prove a theorem allows you to add to the ledger of "things that are true" (which certainly has value, like you mention), but unless the proof is understandable, you don't harvest any of the other fruit that would normally come over the course of proving the theorem "the natural way" (new abstractions to ponder, new conjectures etc). I would argue that Mochizuki's "proof" occupies the same territory as a 100 GB formal logic proof generated by a computer, if the end result is that the proof is not communicable in a way that other mathematicians can relate to. I'm not against creating machine generated proofs. We just shouldn't pretend they have the same status within "mathematics as a social construct" that a human written proof does.