With the discussion flaring up again, let me try to copy it to
discourse (using the email address above).
Regarding, what have people been doing to reach mathematicians. Let me
mention a few initiatives:
https://mapcommunity.github.io/
https://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath
Newton Institute:
https://www.newton.ac.uk/event/bpr
IAS:
https://www.math.ias.edu/sp/univalent
IHP:
https://ihp2014.pps.univ-paris-diderot.fr/doku.php
Moreover, I believe Egbert Rijke has a point:"
- Our communities are simply too small
- Our papers donât get published unless theyâre about new stuff. âThe
definition of a scheme in Coqâ doesnât get favorable reviews.
- We do some fashonable maths: higher topos theory, higher group
theory, some big theoremsâŚ"
https://twitter.com/EgbertRijke/status/1226948002654380033?s=20
I would also add the Mathematical Components book, which was tailored to âmathematically inclinedâ readers: https://math-comp.github.io/mcb/
There are plenty of papers in regular software engineering (in conferences like ICSE, ISSTA, ASE) that are published even though they are not about (mostly) ânew stuffâ, since it is permitted to do replication studies, empirical investigations, etc. For example, a âreplication studyâ in formal mathematics could encode 10+ radically different proofs of the same theorem and and compare them on a set of measures, such as lines of proof script, proof checking time, etc., all while contributing to big formal libraries. (Multiple redundant proofs were also mentioned by Kevin Buzzard towards the end of his latest blog post.)
I donât think itâs impossible to create an ecosystem for this kind of work, but one fundamental choice is whether ITP conferences should have a âproof engineering trackâ, or SE conferences should have an âITP trackâ, or both. Personally, Iâve found the ITP community much more welcoming to engineering research than the SE community to engineering techniques applied to formal proofs.
1 Like