既存の証明系の問題

1. 名前の管理が甘い、名前空間が粗末
2. ユニコードを考慮してない。アスキー偏重。
3. Mizar以外は、スクリプト言語またはそのシンタックスシュガー。
4. ブロック構造を意識してないか曖昧。
5. 文書構造を意識してないか粗末
6. 型クラスがあと付けで歪んでいたり問題を抱えていたり
7. 型クラスがダメなのはインスティチューションを考慮してないから。
8. オーバロードや型強制のメカニズムがわけわからん。
9. パッケージマネージャー、ビルドシステム、アーカイブサイトなどを考慮してない。
10. 計算機代数システム（CAS）との連携が不十分。
11. ドキュメント・システムとして不十分。
12. コミュニケーションや通知機能がないし、想定もされてない。
13. 証明オブジェクトが人間にとっては難読過ぎてい無意味
14. フォワード証明かバックワード証明のどちらか一方しかサポートしてない。
15. 論理資源の管理機構が整備されてない。