Stream: Miscellaneous

Topic: Experimental Mathematics Special Issue on ITP in Mathematics


view this post on Zulip Karl Palmskog (May 18 2020 at 19:57):

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/

4/ 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???) Deadline for submission: Dec 31st, 2020

- Alex Kontorovich (@AlexKontorovich)

view this post on Zulip Karl Palmskog (May 18 2020 at 20:24):

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

view this post on Zulip Pierre-Marie Pédrot (May 18 2020 at 21:50):

@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:

view this post on Zulip Karl Palmskog (May 18 2020 at 22:14):

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)

view this post on Zulip Karl Palmskog (May 18 2020 at 22:17):

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...

view this post on Zulip Christian Doczkal (May 19 2020 at 08:01):

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?

view this post on Zulip Théo Zimmermann (May 19 2020 at 11:03):

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.

view this post on Zulip Bas Spitters (May 19 2020 at 12:16):

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)

view this post on Zulip Karl Palmskog (May 19 2020 at 15:28):

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)

view this post on Zulip Karl Palmskog (May 19 2020 at 15:53):

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).

view this post on Zulip Pierre Courtieu (May 19 2020 at 16:19):

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?

view this post on Zulip Karl Palmskog (May 19 2020 at 16:23):

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

view this post on Zulip Karl Palmskog (May 19 2020 at 16:37):

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?

view this post on Zulip Théo Zimmermann (May 19 2020 at 16:41):

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".

view this post on Zulip Théo Zimmermann (May 19 2020 at 16:43):

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.

view this post on Zulip Théo Zimmermann (May 19 2020 at 16:44):

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).

view this post on Zulip Théo Zimmermann (May 19 2020 at 16:46):

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: Aug 14 2022 at 12:03 UTC