AGISim (Artificial General Intelligence Simulated world) is a framework for the creation of a sensory-rich simulated 3D world for AGI research, allowing AGI and human controlled agents to interact within different rich ‘contexts’.
Lojban is a constructed language with hundreds of speakers, based on predicate logic. Thus, it is particularly suitable for communication between humans and AGIs.
Translating Mizar to KIF
Mizar is a repository of mathematical knowledge, available online but in a complex format that is difficult to feed into AI theorem-proving systems. In six months, a qualified individual could translate Mizar to KIF, a standard predicate logic format, which would enable its use within theorem-proving AI systems, a crucial step toward AGI systems that can understand themselves and the algorithms utilized within their sourcecode.