>>617
>>1)Lean語の方に何か追加するか
>新たな公理の追加はNG
>これわかんないやつは素人

素人はおまえ
反例を列挙しよう

1)ZFCの前、"Zermelo set theory" https://en.wikipedia.org/wiki/Zermelo_set_theory
 では、公理はZFCと異なる形で与えられていた
 すなわち、ZFCにおいて加えられた公理も沢山あるよ
2)他に 有名な公理例で ”Grothendieck universe” https://en.wikipedia.org/wiki/Grothendieck_universe
 グロタンディーク宇宙公理 は、望月IUT IVでも特筆での解説があるよ

つまりは、一般凡人は、 新たな公理の追加はNGだが
しかし、数学天才には 新たな公理の追加は"G"なのだ
果たして、望月氏は 数学天才がどうか? そこが問題だ by ハムレット