- improve many features (translation methods, problem generation, etc.)
- make ATP for proof assistants and real math stronger and stronger
- make interesting AI systems using complementary approaches (learning, theory development, etc.)
- when strong ATP available (seems now), use as a semantic filter for (semi)automated formalization
- make it a part of the wiki for Mizar (http://mws.cs.ru.nl/mwiki)
- try to import ATP-explained Mizar into other proof assistants
- etc.
Josef Urban
2011-01-14