About punctilious

Punctilious is a math proof assistant python open-source development project. In clear: it intends to facilitate the study and development of mathematical proofs by human beings.

There exists multiple math proof assistants, including:

• Coq

• Isabelle

• Lean

…and many more. The proof assistant page on Wikipedia contains a general-purpose comparison of these.

In contrast, punctilious is a ridiculous Lilliputian with neither the length, nor the breadth of these time-proven systems.

So why develop yet another math proof assistant?

Besides being fun and a thrilling learning experience, the focus points of punctilious are:

• Human-friendly and developer-friendly inputs (i.e.: write math as we learn it)

• Ease of use

• Human-friendly and developer-friendly outputs (i.e.: readable)

Punctilious does not pay much attention to:

• Performance (i.e. for large-scale proof applications)