>>294
詳しくないけど公理的な型システムの上で数学するのがトレンドで
型の制約条件を解く手法としてSAT/SMTソルバの性能向上問題があると思うわ（深層学習でこの層を最適化）
あとAI関係ないけどIsabelleのSledgehammer見たいな機構で自動的に証明を使い回すとか