I noticed that some of the Wikipedia.org entries that describe proofs of theorems also contain links to proofs of these theorems formalized in the Mizar proof assistant (example). There was one particular entry that had the Mizar proof code embedded directly in the Wikipedia entry, but I could not find it just now.
Apart from Wikipedia, there are other similar websites, like ProofWiki.org. It seems to me that providing formal proofs or links to formal proofs of theorems formalized in a proof assistant as part of such Wikipedia entries could be beneficial for two reasons:
- Improvement of the popularity of the proof assistants.
- Improvement of the quality of the Wikipedia entries (e.g., improvement of the consistency of the notational conventions used across different Wikipedia entries).
However, it seems to me that the process of integration could and should be automated. Essentially, mathlib already attempts to provide something similar for Lean. Another project that comes to my mind in this context is IsarMathLib developed in Isabelle/ZF by Slawomir Kolodynski. The latter project, perhaps, is more consistent with what I would envisage the integration with a Wikipedia-like website would look like, as it is closer to what I would consider being human-readable by someone not proficient in any proof assistant/type theory.
I believe that the problem of integration is two-fold:
- The formal proofs in the Wikipedia entries need to be updated when the proofs change in the library of formalized mathematics. It would also be beneficial to provide clickable hyperlinks to the definitions and/or other theorems: these links would need to lead to other Wikipedia entries.
- The proofs need to be made as close to being human-readable as possible (related question).
The primary question is whether there exist any other ongoing projects aimed at the integration of the proof assistants with encyclopedia-like websites? The secondary question is whether you can think of any reason why such a project would not be a worthwhile undertaking?