Roadmap

We list here some high-level intentions regarding the future development of punctilious.

Formalization of Math theories

  • Continue the formalization of real analysis from Tao 2006

  • Document (properly) all inference rules

  • Formalize naive set theory

  • Formalize propositional logic

  • Formalize fundamental geometry

  • Formalize the meta-theory of punctilious

Human-friendliness

  • Provide simple to understand error / information messages when invalid inputs are provided to inference functions

  • Support import math from natural math text (ASCII, Unicode, and LaTeX)

  • Support two-columns proofs output

  • Support PDF export

Developer-friendliness

  • Support export to and import from punctilious JSON

  • Support export to and import from punctilious XML

  • Support export to and import from punctilious CSV