> in mathematical writing, what is actually written is the tip of a gigantic iceberg of implied reasoning and background scenery
The programming equivalent of this as I see it is a program depending on lots of libraries encapsulating that "implied reasoning". And you can manage a program even with tens of millions of lines of code in libraries. And it doesn't make the program itself larger because that library code is reusable, you can also use it in other proofs. Yes, it's incredibly hard to manage such a code base, you also need extensive documentation, something like "literate programming" - but it's not intractable.
You would have to write a big part of mathematics as library code, probably a multi-decade length project - but the benefits seem huge! "Translating" mathematics in such a form could augment a mathematicians brainpower "manymany....manyfold" and could be just as important as, let's say, a cancer research project taking decades and tens of millions in funding, but it should worth it! Imagine that hundreds of "less talented" mathematicians could handle problems that only a handful of people can understand today (with the guidance of the "real geniuses", of course), revolutionizing many fields of science through the consequences of their results.
As an analogy, when people used roman numerals, only a handful of highly educated people could do complex calculations, but nowadays we all have more than basic arithmetic knowledge, thanks in large part to a "change of language". I think a "change of language" could really make mathematics a less "elite only" field (though I have greater hopes for letting "AI systems" give a helping hand than for letting "lesser mathematicians" do some of the work, in the end one can't predict what will make the most difference - hardware or wetware, it's still computing power, and, as the complicated software problems are solved, more and more of the computing power can translate into "mathematical reasoning power" I think).
The QED project was started in 1993 to build a database of all mathematical knowledge. It died out because formalized mathematics does not yet resemble traditional mathematics. All existing theorem provers and proof assistants such as Mizar, HOL, and Cow have major shortcomings. Very few people are working to improve formalized mathematics because there isn't any compelling profitable application of fully formalized mathematics.
...so it's one of those "someone has to do it to prove it can be done" or "someone has to first make it work to prove it's useful" problems?
Hopefully there are a few madmen to start working at it and they will be wise enough to do it all "in the open": open source code and publication of all developments, "blog stye", instead of the "talking about only after you've really understood it" approach. I would throw a helping hand on the programming side and maybe devops, even throw a few bucks at it if one were to crowd-source and crowd-fund such an effort ...just because I find it "so cool". And I'm sure there are others that would help any group of "brilliant madmen" trying to do this, even without any imaginable profitable applications. But for now, I'm trying to wrap my head around what the QED project was trying to do and what it did... thanks for the directions to them!
The programming equivalent of this as I see it is a program depending on lots of libraries encapsulating that "implied reasoning". And you can manage a program even with tens of millions of lines of code in libraries. And it doesn't make the program itself larger because that library code is reusable, you can also use it in other proofs. Yes, it's incredibly hard to manage such a code base, you also need extensive documentation, something like "literate programming" - but it's not intractable.
You would have to write a big part of mathematics as library code, probably a multi-decade length project - but the benefits seem huge! "Translating" mathematics in such a form could augment a mathematicians brainpower "manymany....manyfold" and could be just as important as, let's say, a cancer research project taking decades and tens of millions in funding, but it should worth it! Imagine that hundreds of "less talented" mathematicians could handle problems that only a handful of people can understand today (with the guidance of the "real geniuses", of course), revolutionizing many fields of science through the consequences of their results.
As an analogy, when people used roman numerals, only a handful of highly educated people could do complex calculations, but nowadays we all have more than basic arithmetic knowledge, thanks in large part to a "change of language". I think a "change of language" could really make mathematics a less "elite only" field (though I have greater hopes for letting "AI systems" give a helping hand than for letting "lesser mathematicians" do some of the work, in the end one can't predict what will make the most difference - hardware or wetware, it's still computing power, and, as the complicated software problems are solved, more and more of the computing power can translate into "mathematical reasoning power" I think).