Mario Carneiro, Lean4Lean: Towards a Verified Typechecker for Lean, in Lean - https://www.youtube.com/watch?v=t0kHC0YxjLc

Lean を Lean で形式化することについて。色々と厄介なところがあるんだなあ。

#型理論 #Lean #Lean4 #定理証明支援系

Coq Platform の "Intro Patterns" にざっと目を通したんだけど、知っていた以上に色々と記法があるんだなあ

#Coq #定理証明支援系 #CoqPlatform

それぞれのタクティックについて、それがどのようにゴールを変えたのか、表示しているのか。

リンク: https://alectryon-paper.github.io/bench/books/proof-by-reflection.html

#Coq #型理論 #定理証明支援系

型理論の宇宙が、よくわからない……

Russell universes と Tarski universes があるらしいんだけど、どちらがよいのかいまいちよくわからない……

Coq と Agda と HoTT Book と Lean は Russell universes を使用しているらしいから、 Russell universes の方から試してみるのがよいのかな……？

Lean が Russel universes を使用していることは Lean のドキュメントに書いてある。

リンク: https://ncatlab.org/nlab/show/type+universe

#数学 #型理論 #定理証明支援系

『ブラウワー順序数の制限と拡張』を執筆しました。

リンク: https://googology.fandom.com/ja/wiki/Special:Redirect/page/9715

#数学 #巨大数 #定理証明支援系 #型理論

Aczel's encoding は、 Set = Σ [X : Type] [X → Set] というようになる帰納型を使い型理論で集合を符号化するという方法なんだけど、ここの X → Set は重複が許されるので実際は多重集合である。この写像を単射だけに限ることで集合にすることが出来て、そうすると更に色々と都合が良い性質を得られるらしい。

#型理論 #HoTT #構成主義数学 #Agda #定理証明支援系

RE: https://mathstodon.xyz/users/mortberg/statuses/111940426219409755

equivalence を弱めた関係を複数定義し、それらの関係を考察し、それにより equivalence ではない場合についても書き換えができるような Coq のプラグインを実装している。

#Coq #HoTT #構成主義数学 #定理証明支援系

RE: https://mathstodon.xyz/users/Jose_A_Alonso/statuses/111968275067608880

Strict inverses - agda/agda-stdlib - https://github.com/agda/agda-stdlib/pull/1156

こういう細かな定義の変更が積み重なっているんだと思うと、面白さを感じる

#数学 #定理証明支援系 #Agda #プログラミング

#数学 #HoTT #構成主義数学 #Agda #定理証明支援系

RE: https://mathstodon.xyz/users/de_Jong_Tom/statuses/111499525477681029

#数学 #プログラミング #トポロジー #計算可能実数 #計算可能性理論 #定理証明支援系 #構成主義数学

RE: https://mathstodon.xyz/users/MartinEscardo/statuses/111439342950964225

#数学 #HoTT #Agda #CubicalTypeTheory #定理証明支援系 #CubicalAgda

RE: https://mathstodon.xyz/users/mortberg/statuses/111379610737862540

#数学 #定理証明支援系 #Lean #型理論

RE: https://mathstodon.xyz/users/tao/statuses/111360218854032278

テレンス・タオが自身の論文を Lean 4 で形式化する途中で議論の間違いを発見したらしい。

#数学 #定理証明支援系 #Lean #型理論

RE: https://mathstodon.xyz/users/tao/statuses/111287749336059662

What's in a Module? - https://thunderseethe.dev/posts/whats-in-a-module/

プログラミング言語のモジュールについてである。

モジュールに大事なのは「名前空間として働く」と「コンパイルの分割の境界として働く」であるとしている。依存モジュールがコンパイル済みでなければコンパイルできないモジュールシステムを「弱い」としている。依存モジュールが未コンパイルでもコンパイルできるモジュールシステムを「強い」としている。

強いモジュールシステムを実現するためには、そのモジュールの中で使う依存モジュールのシグネチャを指定しておかなければならない。その労力が、強いモジュールシステムの普及のネックとなっている。 "Mixin' Up the ML Module System" (Andreas Rossberg, Derek Dreyer) が実装するモジュールシステムが、それを解決するかもしれない。

これは余談だけど、関数の定義の内部までに依存する定理証明支援系では強いモジュールシステムを使えないか使う意味がなさそうそうなので、強いモジュールシステムを採用する時は、それが課題となりそう。

#プログラミング #関数型プログラミング #定理証明支援系

Functional Programming in Lean - https://leanprover.github.io/functional_programming_in_lean/

Lean での関数プログラミング言語についての文書である。 Haskell の IO モナドは State RealWorld だけど Lean の IO モナドは ExceptT IOError (State RealWorld) であるのが面白い。

#数学 #プログラミング #関数型プログラミング #定理証明支援系 #Lean

RE: https://mathstodon.xyz/users/Jose_A_Alonso/statuses/110450764667925372

Lean 4 の UI を拡張できるようにして、証明の中の式を木などの図に変換して表示できるようにしたらしい。

#数学 #定理証明支援系 #Lean

RE: https://mathstodon.xyz/users/Jose_A_Alonso/statuses/110746832924388601

#数学 #型理論 #定理証明支援系 #Agda #構成主義数学

RE: https://mathstodon.xyz/users/MartinEscardo/statuses/110504563233350460