Functional Programming in Lean - Functional Programming in Lean
Functional Programming in Lean by David Thrane Christiansen Copyright Microsoft Corporation 2023 This is a free book on using Lean 4 as a programming language. All code samples are tested with Lean 4 release 4.1.0. Release history January, 2024 This is a minor bugfix release that fixes a regression in an example program. October, 2023 In this first maintenance release, a number of smaller issues w
Let’s Use An Automated Theorem Prover To Verify Video Games; I Swear This Is More Fun Than It Sounds
Division by zero in type theory: a FAQ
Hey! I heard that Lean thinks 1/0 = 0. Is that true? Yes. So do Coq and Isabelle and many other theorem provers. Doesn’t that lead to contradictions? No. It just means that Lean’s / symbol doesn’t mean mathematical division. Let denote the real numbers. Let’s define a function by if and . Does making that definition give us a contradiction in mathematics? No, of course not! It’s just a definition.
The Future of Mathematics?
As a professor of pure mathematics, my job involves teaching, research, and outreach. Two years ago I got interested in formal methods, and I learned how to use the Lean theorem prover developed at MSR. Since then I have become absolutely convinced that tools like Lean will play a role in the future of mathematics. With the help of a team of enthusiastic undergraduates at my university, we have be
定理証明リンク集
定理証明、特に定理証明支援系(Proof Assistant)はその存在こそ少しずつ浸透しつつあるような気がしないでもないけれど資料とか全然まとまってないのが不便だなと前々から思っていたのでリソースをまとめておきます。 これも追加してほしいみたいなのあったら教えてください。 Proof Assistants 始めるなら次の中から選ぶのがよいと思います。 Coq Calculus of constructionsベースの型システムとリッチなコマンドを備えた言語 このリストの中では最もコミュニティが大きい、入門書等も豊富 型システムと項を書くためのGallina, コンパイラへの命令を記述するためのVernacular, タクティクスの定義に使うLtacなどの言語が混ざって出てくるのが初心者には混乱必至 結構複雑な言語なので使いこなすのはそれなりに大変 Agda Martin-Löf type
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
The Hitchhiker's Guide to Logical Verification
Reflexive tactics for algebra, revisited
Egglog 2: Automatically Proving the Pullback of a Monic is Monic
Sandy Maguire: A New Kind of Programming: Tactic Metaprogramming in Haskell @ZuriHac21
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
From Zero to Factorial
Towards Tactic Metaprogramming in Haskell :: Reasonably Polymorphic
http://arxiv.org/pdf/1910.10703
Arend
Reddit - Dive into anything
Reddit - Dive into anything
Cedille Cast #4: Deriving Equi-recursive types with Tarski's Fixpoint Theorem
Computer Scientists Close In on Perfect, Hack-Proof Code
GitHub - latte-central/LaTTe: LaTTe : a Laboratory for Type Theory experiments (in clojure)
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle