There must be a pretty good chance that AI really will happen in the 21st Century. Factasia wants a piece of the action. The logical techniques for fully formal mathematics have been known for a century. Putting them into practice is still a challenge; a software engineering challenge.

A short story about the mechanisation of mathematics. Its primary purpose is speculation about what could be done, and how, but there's a bit of background material about what has been done. A megaproject involving lots of information technology.

There must be a pretty good chance that AI really will happen in the 21st Century. Factasia wants a piece of the action.

What is Intelligence? By a way of clarifying the scope of the field and identifying the particular interests of Factasia, we seek a definition of intelligence which is not homo-centric. There are many rich connections between philosophy and AI, particularly between analytic philosophy and logical AI. This extravagent label covers Factasia's interest in the AI project of the (next!) millenium. The world transformed by the evolution of intelligence in cyberspace.

Automation of deductive reasoning is the subdomain of AI of greatest interest to Factasia. Crystal clear problems, widespread applications. Mathematics provides the most complex applications of deductive reasoning and is therefore a testbed for the automation of reasoning. Here we consider the transition from powerful but non-intelligent programs to intelligent mechanised mathematics. Topography Factasia's architecture for AI places pure logic at the centre of it all.

The logical techniques for fully formal mathematics have been known for a century. Putting them into practice is still a challenge; a software engineering challenge.

Background and Motivation Leibniz dreamed of mechanising reason and mathematics but didn't have the wherewithall. Lots of people still want to do it, and think logic, computers and a bit of graft will do the trick. Formal Foundations This whole enterprise depends upon the fact that mathematics can be reduced to logic. So you need to know what a formal logical foundation system is.

Developing Formal Maths A first goal is to be able to productively develop mathematical theories, in collusion with computers, with all theorems and proofs formal and machine checked. Applying Formal Maths A more ambitious (and maybe more profitable) goal is to exploit the formal methods to get computers which are good at applied mathematics.

A short story about the mechanisation of mathematics. Its primary purpose is speculation about what could be done, and how, but there's a bit of background material about what has been done.

A megaproject involving lots of information technology.

1. Conceptions First we look at some of the varied conceptions of the Global Brain elsewhere on the internet.	2. Dimensions Then we analyse some of the dimensions of variation in these different conceptions of the Global Brain, and begin to position Factasia.
3. Cogitations Next we have a serious think, integrate the Global SuperBrain into the Factasia philosophical worldview, and identify two quite different superbrain projects for Factasia to run with.
The idea of a "control system" is taken from cybernetics and applied on the global scale to the problem of realising a better world.	The Global SuperBrain as Hyper-Rational Artificial Intelligence. An intelligent automation of the entire field of a priori knowledge, including mathematics and its applications in science and engineering.

:

---

© created 1995/4/25 modified 1999/10/12