Brief: Intended as a "universal database of mathematical knowledge"
Jump To: Parent Description

  • As Leibniz said, calculemus! The idea is that real life problems are reducible to computational problems, which are reducible to mathematical problems. Thus, Algorithmic Information Theory is applicable, which says that if a set of mathematical problems contains t-bits of information (Shannon entropy), and our program for solving these problems contains less than t-bits of information, then it is impossible to solve these problems from these programs. This is an example in itself of epistemic reasoning deciding practical reasoning, for we know that it is necessary to increase the Shannon entropy or rather Kolmogorov complexity of our programs in order to have chance to solve more problems. The easiest practical method of achiving this is to collect software that people have written. We are working to mechanize this ( ) argument, at least the deductive components) into agda at present. We are still working to formalize the abductive component into an argumentation schema for practical reasoning. In order to increase the K-complexity of our systems, we are developing a sequence of mathematical formal libraries which are able to solve strictly more computational problems. For instance, databases of known computational complexity results could aid algorithms for computing the resource complexity of various programs generated by metaprogramming and/or program synthesis. See also: