Initial agenda of the meeting:

• Advances on the paper
• Announce mathcomp-analysis on mathcomp dev mailing list?
• What is everyone doing?
• PR statuses

Participants

• Reynald Affeldt
• Cyril Cohen
• Marie Kerjean
• Assia Mahboubi
• Laurence Rideau
• Damien Rouhling
• Pierre-Yves Strub

Summary

Next Meeting

• Cyril will open a poll for a meeting in January

Communication

Web communication

• We should have a visible website
• We should advertise the library on Coq's channels
• Cyril opened a Gitter channel here

Paper

• Back to the tension between lack of space and lack of advertisement: we will write a journal paper as if it was for LMCS (better delays than MSCS) and then decide if we extract a part for a conference or if instead we present the library in workshops
• Goal: clearly explain our formalization methodology
• Target audience:
  • "math researchers" (typically people on Lean's Zulip channel)
  • people from program certification (e.g. measure theory is required for the certification of probabilistic programs)
  • people interested in the proof of numerical and symbolic computer systems

Misc.

• To convince people, the library should have access to an adapted version of Interval and its dependencies
• We should get in touch with Silvain Rideau about ultra-filters
• Also true for mathcomp: we are not small scale extremists! We should make it clear that using tactics such as lra and ring is perfectly fine with us.

Prop vs bool

• Assia informed us of discussions about sProp (elements of P : sProp are convertible)
• We discussed the possibility of replacing bool/Prop with sProp + a decidable class