>>548
年頭ブログ記事の内容を私なりに要約してみると
iutでは
(1) species/mutationの理論をメタ理論として
「一階述語理論としてのZFC」を扱えば
「不定元のような論理式」を扱うことができる
(2) それをleanで形式化してほしい
ってことでしょうか
(2)の動機はもちろん(1)に対する疑義を否定するためです
(1)のような理論は（現時点で）存在しません
類似例として思いつくのはモデル理論ですが
制約が多く(1)のように都合よく使えるものではありません
しかしブログ記事では相変わらず(1)は自明に成立としているので
何か壮大な勘違いをしていると思います
結局、自明を強調して詳細な説明を拒否する箇所に
手品のタネが隠されているということだと思います

（ブログ記事より引用）
＞species/mutationは、特に難しい話でもなく、取り立てて
＞新奇性のある話でもなく、多くの数学者が当たり前に脳内で
＞無意識のうちにこなしている処理を、（同様の概念が明示的に
＞記述されている適切な文献が見付からなかったために）
＞ただ自分で明示的に記述してみただけ
（中略）
＞多くの基礎論の専門家も認めている通り、species/mutationは
＞全然難しい話でも、新奇性のある話でもない。