26/07/25 21:53:16.26 AuqA/R3q.net
>>505 補足
>まあ、現実を
>誤魔化さずに素直に 直視すること
>そこが、基本で出発点ですよ
みなさん
コメントありがとう
繰り返すが
１）望月、星、加藤で話をして 現状のLeanのコードを含めて
あらいざらい、オープンにすること
２）望月＋星他 一族で 今回の中間報告への応答を発表すること
まず、すなおに Lean形式化未達であること
その原因についてを述べて
その後,これからどうするのか？ 計画と見通しを述べる
３）その後、Lean形式化達成に向けて、シンポジュームとか
オープンな議論の場を持つ（議論は公開する）
これを繰り返す。その中で、Lean化達成できればGood！