I would also be very interested in seeing some smaller stepping stones implemented -- I imagine that creating an AGI (let alone FAI) will require massive amounts of maths, proofs and the like. It seems very useful to create artificialy intelligent mathematics software that can 'discover' and proof interesting theorems (and explain its steps). Of course, there is software that can proof relatively simple proofs, but there's nothing that could proof e.g. Fermat's Last Theorem -- we still need very smart humans for that.

Of course, it's extremely hard to create such software, but it would be much easier than AGI/FAI, and at the same time it can help with constructing those (and help in some other areas, say QM). The difficulty in constructing such software might also give us some understanding in the difficulties of constructing general artificial intelligence.