How to do Math in programming

**デフォルトの名無しさん** · 2024/03/21(木) 09:41:43.97

What is "mathematics in programming?"

Some well-known facts in mathematics are difficult to prove using a computer.
For example, the Leibniz series

1 - 1/3 + 1/5 - 1/7 + ...

is exactly equal to π/4, but calculating this series directly is impossible because it requires infinite computation.
However, from the theorems of analysis, this equality can be shown. Thus, if all these theorems are formulated in terms of logic symbols, the proof is reduced to a finite algorithm.

Some might say that a "proof assistant" or "theorem prover" would make this possible.
However, the language of proof assistants is too complicated to describe proofs of non-fundamental theorems, so proof assistants are used only to check proofs that have already been solved.
This is far from doing mathematics.

My question is where do mathematical ideas come from and whether programming can help yield them?

**デフォルトの名無しさん** · 2024/03/21(木) 10:47:44.36

fuck your asshole

**デフォルトの名無しさん** · 2024/03/21(木) 11:56:07.97

Theorem Proving in Lean 4　日本語訳
https://aconite-ac.github.io/theorem_proving_in_lean4_ja/title_page.html

定理証明なら、今はCoqよりこっちなんかな

**デフォルトの名無しさん** · 2024/03/21(木) 12:07:26.54

依存型を使った定理証明入門

https://zenn.dev/blackenedgold/books/introduction-to-idris/viewer/theorem-prooving

定理証明の流れは

命題を型に変換する
型がnon-emptyであることを示す

なので、実行時に型チェックすれば動的型付け言語でも証明はできるわけか
ただ、全称型とか存在型とかをどうやって表すのかがわからない

**デフォルトの名無しさん** · 2024/03/21(木) 23:49:19.66

より直感的なシンタックスと、命題のインタフェースを簡単に変換できる機能がほしいな

**デフォルトの名無しさん** · 2024/03/23(土) 09:58:52.52

命題 → 型

偽 → ∅
not A → Hom(A, ∅)
真→ not ∅

AかつB → 直積A×B
AまたはB → 直和A⊕B

AならばB
= not A または B
= (not A)⊕B
= Hom(A, ∅)⊕B
～ Hom(A, B)　※ 真偽が一致する

**デフォルトの名無しさん** · 2024/03/24(日) 22:31:53.90

プログラムはバイト列にコンパイルされるから、すべてのプログラムは高々可算個になるのだが、なぜ非可算集合をふくむ論理を扱えるんだ？

**デフォルトの名無しさん** · 2024/03/24(日) 23:10:41.69

量化してるからだよ