Re: Coq vs lean for classical analysis

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:
Newton Institute:

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

I would also add the Mathematical Components book, which was tailored to ‘mathematically inclined’ readers:

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