山下サーベイ『A proof...』のRemark 3.4.4.
＞(1) It seems difficult to rigorously formulate the
＞meaning of "group-theoretic characterisation".【以下略】
＞(2) (Important Convention) In the same way, it also seems
＞difficult to rigorously formulate "there is a group-
＞theoretic algorithm to reconstruct" something in the sense
＞of mono-anabelian approach【中略】(If we use the language
＞of species and mutations (cf. [IUTchIV, §3]), then we can
＞rigorously formulate mono-anabelian statements without
＞mentioning the contents of algorithms).

残念ながら"language of species and mutations"は
rigorousな（＝形式化できる）数学ではありません
従って単遠アーベルの中心的概念である復元・アルゴリズム云々は
単なるレトリックに過ぎません
レトリックを使うこと自体は否定されるようなことではないですが
定理の記述に使うのは避けるべきことですし
証明をそれで済ませるなどもってのほかです