証明論や順序数解析は私には全くわからないからAlweさんにLeanを無理やり学ばせてやらせよう　形式証明を書くこと自体はAI/LLMでチャラにできるから大丈夫ですよきっと

@SnO2WMaN これなんですか

@Alwe_Logic つい先日Goodstein列の停止性のPAからの証明不能性をFFLのフレームワーク上でClaudeで形式化させたという連絡が来て、それ自体は正しく出来ているだろうと確認してるのですが、如何せん形式証明のコードがカオスなので実際には1から再設計していったほうが良いだろうなと結論づけています(1)

@Alwe_Logic で、今月ずっと実験した結果（他のソフトウェア開発の領域と同じように）、現状はおそらく人がスケッチや証明の方針、全体的な設計のデザインなどを与えたほうが良いだろうと思っているのですが、証明論や順序数解析は少なくとも私の手に負えないので(2)

@Alwe_Logic 私が知る中で最も証明論に詳しい人であろうAlweさんにせっかくならこういう機会でLeanをやってみてはどうでしょう？という提案でした。逆に言うとスケッチさえ渡せば煩雑な計算とかは力任せで解くので逆に相性良いのでは皮算用もあります（この分野については全く知らないので嘘かもですが）

@SnO2WMaN なるほどなぁ。私に形式化をする余裕と、お金がないという悲しみがあります

@Alwe_Logic ；；（証明を実際に書かせる部分は私がやるので、暇だったらまた連絡してください）

@SnO2WMaN 修論が終わったら……(もしなにか話すとしたらMLGあたりで話せたら良さそうだなと思います)

@SnO2WMaN PAの無矛盾性証明の部分をfactにしてしまっていいなら、証明はこの論文に沿って行うのがいいと私は思っています arxiv.org/abs/1405.4484

@Alwe_Logic PAの無矛盾証明はそれこそ出来ていて（モデルにも、無限体系のカット除去によるものでも）、Kirby-Parisの定理以上の証明論的な応用やマイルストーンなどを私では上手く設定することが出来ない（あるいはより良い地図を持っている人がいる）という話です

@SnO2WMaN どの方向性で一般的にしていきたいかにもよると思うのですが、slowing downの形式にしておくと少なくともε_0周りのものだったら上の論文で十分というのが私の意図で、もっと一般のものまで考えたいならFriedman-Sheredあたりを形式化するのが筋が良さそうだなぁという気持ちです。