Is this supposed to be in jest, or serious? If true, I guess we can scrap most of CPP reviewing...

Step 1: The board will decide whether the theorems stated are of sufficient importance to warrant inclusion,

and

Step 2: Just run the code! If it compiles, it's right! No need for refereeing!

(Isn't that incredible???)

Source: https://twitter.com/AlexKontorovich/status/1261350127286890499 Background: https://think.taylorandfrancis.com/special_issues/interactive-theorem/

IMO, proper ITP artifact reviewing is super tough, and should involve lots of tooling (like dependency checking, axiom tracking, mutation analysis, ...) by experienced users/developers of the system

@Karl Palmskog if this is indeed real, then paper bonanza from our community! Let us never forget the one bitcoin I hard-earned by `Definition False := True.`

:money_with_wings: :paper: :hammer:

Twitter account has 5000+ followers and seems consistent with https://math.rutgers.edu/~alexk --- he even gets some comment on the original tweet from Fields medalist Gowers: https://twitter.com/wtgowers/status/1261668207880011778

@agolian @AlexKontorovich I wonder whether one could speed up the process by developing corpora of "trusted results" whose correctness was not in any serious doubt and which were therefore considered fair game to use to prove other things formally. 1/

- Timothy Gowers (@wtgowers)he [Gowers] is seemingly not yet aware of a certain axiom-free library of what one might call "components" which one might use to "prove other things formally" --- or does he actually mean a corpus of informal math? If the latter, unclear to me how it would help...

Maybe someone (with more "standing" than me/us) could write one or both of them an email, inform them, and ask them to clarify what they mean?

FTR there was a reply from someone in the field of ITP who explained that this reviewing process might be a bit simplistic. I just bumped the comment to the top of the replies by liking it with my own Twitter account and Coq's Twitter account.

I've linked to ITP and CPP:

https://twitter.com/BasspittersBs/status/1262718119090495489

@AlexKontorovich @stuckintheory The formalization of (mathematical) proofs is a specialized discipline with well-established practices. Will you be following the same standards? E.g. https://popl21.sigplan.org/home/CPP-2021 https://waset.org/interactive-theorem-proving-conference-in-july-2020-in-paris

- Bas Spitters (@BasspittersBs)Alex cited this from the paper call in response to issues raised (https://twitter.com/AlexKontorovich/status/1261651977739665412):

Any code must be extensively documented with comments that make it readable by a professional mathematician with little formalization experience

I guess it's all fine if it's surface-level readable, i.e., no semantic exploration needed? Maxime's puzzles comes to mind...

@stuckintheory These are very good points. The call for papers explicitly states: “Any code must be extensively documented with comments that make it readable by a professional mathematician with little formalization experience” So this fact will need be to ascertained (by referees...)

- Alex Kontorovich (@AlexKontorovich)I still think it would be a good idea if someone with sufficient credentials/standing emailed Alex to explain why "surface level inspection" and reading comments are simply *not enough* (along the lines originally suggested by Christian above).

Maybe linking to this:

http://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/

Would give a hint of the real work needed?

Assia's writeup is also good: https://project.inria.fr/coqexchange/checking-machine-checked-proofs/ and also https://proofartifacts.github.io/guidelines/

To be honest, this [instructions for reviewing Coq formalizations] is again something that could be crowdsourced specifically for Coq and maintained in coq-community IMO. Many people are not aware of `coqchk`

and `Print Assumptions`

and so on. Or perhaps it even belongs in the manual @Théo Zimmermann?

Yes @Karl Palmskog, I feel like it would be a good addition to the reference manual. You may be aware that the reference manual has been completely restructured in 8.12 (cf. https://coq.github.io/doc/master/refman/). CEP#43 that introduced this change contained the following about the new "Using Coq" part:

We expect to add one or two new chapters about project management / proof engineering (including how to review a Coq formalization) in the part entitled "Using Coq".

Note that there will soon be a call for crowdsourced help to improve the current state of the reference manual, including by writing new content about such topics.

It could even be included in the 8.12 release if it is merged by the 8.12.0 release date (expected early July, ideally for the Coq workshop).

That being said, this could be completed by a coq-community repository going more in-depth on "case studies" inspired by cases encountered in a real reviewer's life.

Last updated: May 31 2023 at 03:30 UTC