MathINsiD is built and maintained by Arnaud Mayeux. Contact: contact@mathinsid.org.
The formalization score, the correctness profile, and the design of this bridge between bibliographic records and formal artifacts are described in:
Arnaud Mayeux, Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge, arXiv:2606.11430. Licensed CC BY 4.0.
Section III of that paper defines the score S(P) and the five correctness classes — certified, corrected, uncorrected, open, untested — that this index stores alongside every score. This index additionally uses a sixth, temporary status, detected, for papers where a formalization artifact is on record but its statements have not yet been individually assessed into the five-class profile above.
Arnaud Mayeux, Formalizing all indexed mathematics as a benchmark for general reasoning, Lecture Notes in Networks and Systems, vol. 2146, Springer, Cham, pp. 393–405, doi:10.1007/978-3-032-35078-7_23.