Comment Comment by infruset If on top of rigorous, you want them to be formally verified in Coq at the same time as they are computed: https://www.lri.fr/~melquion/doc/18-jar.pdf parent infruset 2 years ago