the main program is transformed into a test of compute_sums.
It seems that the metas are not needed anymore.

and a bit of cleaning at the same time

  Fix: shortcut for provers which are unknown

Johannes, Yannick: yes this is what you think (good news)
but this is not yet completed (bad news)

(we do not have to use the ghost construct here, but it looks nicer)