LEAN形式化の過程で幾つかの定理をブラックボックスとして
使うのは普通のことです
例えばBuzzardのFLT形式化プロジェクトでも1990年以前の結果で
形式化されてないものはブラックボックスとして使うと言っています
しかし今回のようにブラックボックスそのものに疑義がある場合
moduloブラックボックスの形式化にどのような意義があるのか不明です
>>70の文書のSkeletal Lean codeが何を示唆しているのか不明です
そもそも>>70の文書はmoduloブラックボックスで形式化するとも
言ってないのでこの議論自体無意味なのかもしれないよ