if you give a recursive enumeration of every real between 0 and 1, that should sufice. such an algorithm, if you indeed possess it and it does what you claim, it would be of great interest to many people.
but...it is highly likely that there is an undiscovered flaw in your algorithm, which might not easily be detectable (especially if the algorithm is of sufficient complexity).
commutative diagrams COULD be proofs. for example p→q is just a small diagram. yes, you have a "different kind of formalizing", but logical need not be lingual. the common usage of diagrams now IS informal, this is true, but formal systems can be created which aren't string manipulation. an example can be found in:
until relatively recently, geometric proofs ("pictures" a la Euclid), were the gold standard of "formal proofs". it's likely that as we accumulate more knowledge, better formal systems using more sophisticated building blocks will emerge.
(by the way, metamath is an awesome site).
why, the uniquely defined impossibly inaccessible cardinal, of course :P