MathINsiD

Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

A compass in the formalization of all indexed and published mathematics.

loading…
formalization
year
connecting…

Correctness profile — how each statement stands against formal verification

certified — formalized and proved as printed corrected — refuted, corrected version proved uncorrected — refuted, no corrected version available open — unresolved, formal statement exists untested or unresolved — no formal counterpart currently detected

a paper marked detected has a known formalization artifact (e.g. a mathlib declaration) that has not yet been assessed into the profile above — formalization is confirmed to exist; how much is not yet quantified.