LeanというはAIではなくプログラム言語の一種で、そのLeanコンパイラ自体は人間が読めるソースコードから作られてる古典的プログラム
つまりNNではないのでシステムにブラックボックスな部分は無い
オープンソースなので世界中の誰でも自分のPCでLeanでの証明プログラムの検証が出来る