13
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • 2
    $\begingroup$ I'm not sure the mathlib crowd would react positively to something of the form "you must now make the following mathlib proofs human-readable as part of a project I'm doing". However I think they would be far more positive to pull requests of the form "here is a pull request which documents what is going on within this proof in order to make it more human-readable". Note also that a mathlib proof of a theorem might be extremely short, farming the work off to other more technical lemmas.What then? $\endgroup$
    – Kevin Buzzard
    Commented Feb 18, 2022 at 19:29
  • 1
    $\begingroup$ @KevinBuzzard The process of making the proofs human-readable would need to be (at least partially) automated. In any case, this is neither something that I would consider doing myself, nor something that is being done by anyone I know. This post is a genuine question combined with an idea that I wanted to share (as part of my commitment to make 10 posts on this website within a reasonably short timeframe :-) ). As for your question about the technical lemmas, they can be provided as part of one or another Wikipedia entry (so long as the links to them exist somewhere). $\endgroup$
    – user9716869 - supports Ukraine
    Commented Feb 18, 2022 at 19:42
  • $\begingroup$ Related: a question about automating the code-to-natural language translation. $\endgroup$
    – march
    Commented Feb 18, 2022 at 20:05
  • 2
    $\begingroup$ For historical record there used to be wikiproofs.org. It was a formalized mathematics wiki created in 2009 by Alexander Klauer which everyone could edit on-line, like the Wikipedia. The formal part was verified by JHilbert, which was derived from Ghilbert, which was based on Metamath). $\endgroup$
    – Slawomir K.
    Commented Feb 20, 2022 at 9:25
  • 2
    $\begingroup$ I have written a proposal that seems to be in the spirit of this question: github.com/SReichelt/slate/discussions/84, with a few implementation ideas (but no actual implementation yet). $\endgroup$
    – Sebastian Reichelt
    Commented Feb 20, 2022 at 12:11

1 Answer 1

Reset to default
8
$\begingroup$

Metamath has a Proof Explorer; here is one entry. This is mostly a visualization of the proof database set.mm.

Because of the nature of the Metamath proof assistant, any new theorems or derived inference rules will get their own name inside the proof database you're currently working in. Most of these theorems are too granular to justify having an article about them, but it would certainly be possible to link to the most important ones from Wikipedia itself or a Wikipedia-like website.

I think this addresses the unidirectional case (from a human-targeted explanation like a Wikipedia article to a web-accessible view of a proof database).

For the bidirectional case, it's not really clear to me what the goal is. Are you trying to mechanically check that the notations and definitions used in Wikipedia-like articles are all consistent with each other?

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ "Are you trying to mechanically check that the notations and definitions used in Wikipedia-like articles are all consistent with each other?" This could be one of the potential goals. Also, Metamath, indeed, provides something that is very close to what I envisaged when writing this question and it is rather imperative that it is mentioned in this thread. Nonetheless, the primary question is still about the integration with the existing "popular" websites. $\endgroup$
    – user9716869 - supports Ukraine
    Commented Feb 18, 2022 at 21:46

Not the answer you're looking for? Browse other questions tagged or ask your own question.