>>617
>＞１）Lean語の方に何か追加するか
>新たな公理の追加はＮＧ
>これわかんないやつは素人

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

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

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