Proofscape modules have their own language, in which you can define deductions (theorems, proofs, and expansions) as well as annotations (interactive discussion and commentary on proofs).
When it is time to link together the steps of a deduction, there is a mini-language for this, called Meson.
- Proofscape Module Tutorial
- Meson Language Tutorial
- Proofscape-flavored JSON