the way math grow, in the big scale of things, is an additive process (locally it can be a big mess of intuitions, fights, and faith. anyway). so, it’s a process on which new theorems are proved by using previously proved theorems, and so on all the way down to the basic axioms of mathematics, which you cannot prove anymore, but accept as true (axioms can be changed such that new mathematics can be created, but that’s another story, for now we just accept those that produce maths that make sense to our perceptible world). this has worked fine so far.

however, this process of building mathematics means that, of course, one must be familiar with the theorems that are gonna provide help on proving the new ones. as we continue developing maths, and we escalates in knowledge, as we invent new branches and theories, and define new fields, things get both more abstract and more of course more numerous. perhaps, up to a point beyond which no human can keep all the necessary information in his brain or simply follow the level of abstraction involved. then, humans will need some help.

in fact, i think that day is already now. computers assist mathematicians into proving their theorems, by formally checking that every theorem, lemma, proof, law and corollary involved in every single step is indeed formally correct. note than i’m not speaking of computational checking (as if maths where about numbers), but really going down to the basics of symbolic logic in every step.

in the other hand, even if we obviate the issue of the volume of a forma prove, as things get more abstract and complex, i guess humans are not that reliable anymore for formal proving and we shouldn’t count on them for formal discussions. then, i suppose, it will be the computer’s job to proof the theorems, and humans job to only propose new ones. cause for creating new theories and propose theorems, you only need some basic understanding and lot of intuition. and at that, we humans are good. so, ¿shall we let the computer do the mechanical part?

*so, to give you an idea, think it like this: in these computer programs, even things like 1 + 1 = 2 are formally proved from the properties of arithmetic. now, i read that even the simple definition of the number “1” requires an expansion of four trillion symbols when expressed formally in such computer systems. not that you need to go that down every time, building maths is like modular design, but still.*