Inter-universal geometry とABC 予想55

**１３２人目の素数さん** · 2024/04/13(土) 15:22:57.08

未だにcontroversialなIU幾何やABC予想に関する会話のサロンとして使って下さい。

荒らしはご遠慮願います。
応援スレとの棲み分けにより、懐疑的な意見も歓迎です
関係者の匿名的な論理的擁護も歓迎です

**１３２人目の素数さん** · 2024/04/30(火) 18:14:21.83

Scholzeさんの例は有名すぎるのでもう一つ。。。Tim GowersさんやTerence TaoさんのMarton conjecture解決の論文も、Lean4での形式化が企画されてますね。
[https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/]

基礎論による形式数学がコンピューターで実装されたことで、確実に実践的な証明と形式化された証明の距離は近づいています。これが今の数学なのです。

**１３２人目の素数さん** · 2024/04/30(火) 18:30:24.97

HoTTだろ。プログラミングで言ったら関数型＋論理型
LeanはC＋から実装しているらしいが、実質的に振る舞いは関数型＋論理型
だからIUTを推進したいなら関連性を論文にするしかないんだよ
無理なら無理で何で無理なのか