Conclusion

Immediately

• Complete the software infrastructure
• Document, release, and maintain

In the Short Term

• TSTP format for models
• Model verification

In the Long Term

• System certification
• Mining the TSTP for proof abstractions and lemmas

Grand Plans

• Make connections between levels
  • Formalized human proofs (Mizar)
  • FOF equivalents (Josef's work)
  • CNF refutations (ATP work)
  • Refutation verification (my students' work)