Karl Palmskog (Nov 06 2020 at 14:14): Karl Palmskog (Nov 06 2020 at 14:14):I see that there is still some MathComp-related code hosted on gforge here that will disappear end of December: http://marelledocsgit.gforge.inria.fr
Specifically, (1) differential dynamic logic and (2) Proof of transcendence for e and pi. The latter looks quite useful and I have not seen it anywhere else. Is there a plan to preserve this stuff somewhere? May I ask that you bring this up on the next MathComp meeting @Enrico Tassi @Cyril Cohen (unless the code has already been moved somewhere and I've missed it)
Enrico Tassi (Nov 06 2020 at 14:15):CC @Yves Bertot
Cyril Cohen (Nov 06 2020 at 14:56):For (2) it is here: https://github.com/Sobernard/Lindemann
Cyril Cohen (Nov 06 2020 at 14:57):We should probably ask Sophie Bernard if we can move it to math-comp and takeover the maintenance.
Yves Bertot (Nov 09 2020 at 08:16):I will discuss the move with Sophie the next time I have her on the phone (less than 2 weeks).
Concerning the specific proofs of transcendence for e and pi, we probably still should preserve them as is, for historical access. I have not checked before writing this short answer, but the sources are probably mentioned in the 2016 CPP paper about it (https://arxiv.org/abs/1512.02791)
Karl Palmskog (Nov 09 2020 at 08:33):can confirm the source link is mentioned in the CPP paper, so makes sense to store original sources referenced in the paper somewhere, e.g., as an attachment to a tag in Sophie's repo
Last updated: Dec 07 2023 at 09:01 UTC