Feature request: include the original problem descriptions in docstrings for the theorem statements

[eric-wieser]

It's quite hard to spot misformalizations when reading the formalization alone. It would be great if the $$\LaTeX$$ description could be included in a docstring (/-- doc -/ in lean, I can't speak for other systems) for the theorems, to make mistakes easier to spot and correct.

[LasseBlaauwbroek]

Seconded for Coq: (** latex *).

[eric-wieser]

Probably also a good idea to have a script that extracts the docstrings from each language, and checks in CI that they are all consistent.

[amit9oct]

Thank you for opening this issue. I agree that something like this will make it easy for the repository maintainers to check the correctness of the formalization itself.

We are planning to add a tool (probably a web page on our main website) that will grab the three formalizations along with informal statements from the GitHub repository and then show them side-by-side. We can also build a local version of this so that the maintainers can see these on their local machines.

The reason for not adding comments in the file is that it will make it hard to maintain the same informal statement in two places, and might create problems when one gets modified but the other does not. If we create a tool for this, then we will not have to deal with any consistency issues which may arise. This will also keep parsing of formalizations simple, for example, if someone wants to just use the formal statement and not use informal statements for their AI tests they will not have to parse and remove the informal statement from the file.

[eric-wieser]

The reason for not adding comments in the file is that it will make it hard to maintain the same informal statement in two places, and might create problems when one gets modified but the other does not.

My recommendation here would be:

• Write a script for each of Coq, Lean, and Isabelle that extracts the doc comment to a json file, mapping problem names to docstrings. I suggest separate scripts since you might find that it is best to parse the Coq code with Coq, the Lean code with Lean, etc.
• Add a test in github's CI that verifies the outputs of these three scripts are identical

CI is a fantastic tool for enforcing consistency.

[eric-wieser]

CI is a fantastic tool for enforcing consistency.

216 adds the docstrings to all the lean files, and uses CI to ensure they are the same as the ones in the json file.