Before choosing theorems for getting proof tokens we cannot avoid making a stand on the underlying foundation (logic, axioms). For my part, I have been Reading and it seems -- personally -- first-order logic is The most common of logics. it would be used to state mathematical theorems by their set theory formulation (using the set membership relation). The logic would need set theory axioms like ZFC. I don't know if this would be good enough, but we still have time for talking about it and may exchange for an alternative. (we do not need to buy into the underlying logic now)