From a6693e40f33c8329d5910a30a89b98739456f2c8 Mon Sep 17 00:00:00 2001 From: thelissimus Date: Tue, 11 Nov 2025 14:27:57 +0500 Subject: [PATCH 1/4] init: proof assistants & websites --- proof-assistants.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 proof-assistants.md diff --git a/proof-assistants.md b/proof-assistants.md new file mode 100644 index 0000000..e17fa30 --- /dev/null +++ b/proof-assistants.md @@ -0,0 +1,24 @@ +# Isbot assistentlari + +Asosiy isbot assistentlari: + +- Agda +- Lean +- Rocq (sobiq Coq) +- Isabelle/HOL + +## Agda + +- [Veb sahifa](https://wiki.portal.chalmers.se/agda/pmwiki.php) + +## Lean + +- [Veb sahifa](https://lean-lang.org/) + +## Rocq + +- [Verb sahifa](https://rocq-prover.org/) + +## Isabelle/HOL + +- [Verb sahifa](https://isabelle.in.tum.de/) From 6d02ebcb4591697c81ef0b050c149d5accf7becd Mon Sep 17 00:00:00 2001 From: thelissimus Date: Tue, 11 Nov 2025 14:29:20 +0500 Subject: [PATCH 2/4] remove: higher order logic flavor --- proof-assistants.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proof-assistants.md b/proof-assistants.md index e17fa30..03d5c7c 100644 --- a/proof-assistants.md +++ b/proof-assistants.md @@ -5,7 +5,7 @@ Asosiy isbot assistentlari: - Agda - Lean - Rocq (sobiq Coq) -- Isabelle/HOL +- Isabelle ## Agda @@ -19,6 +19,6 @@ Asosiy isbot assistentlari: - [Verb sahifa](https://rocq-prover.org/) -## Isabelle/HOL +## Isabelle - [Verb sahifa](https://isabelle.in.tum.de/) From 486cb1dd4a6e0ac4550ea71ebe25a40318de2c90 Mon Sep 17 00:00:00 2001 From: thelissimus Date: Tue, 11 Nov 2025 14:40:20 +0500 Subject: [PATCH 3/4] better introduction --- proof-assistants.md | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/proof-assistants.md b/proof-assistants.md index 03d5c7c..76f325b 100644 --- a/proof-assistants.md +++ b/proof-assistants.md @@ -1,11 +1,6 @@ # Isbot assistentlari -Asosiy isbot assistentlari: - -- Agda -- Lean -- Rocq (sobiq Coq) -- Isabelle +Isbot assistenti (Inglizchada "proof assistant"), yohud (interaktiv) teorema isbotlovchi (Inglizchada "(interactive) theorem prover") [formal isbot](./formal-proof.md)lar ustida ishlashga yordam beruvchi dasturlardir. Bunga [Agda](#agda), [Lean](#lean), [Rocq (sobiq Coq)](#rocq), [Isabelle](#isabelle) va boshqalar misol bo'la oladi. ## Agda From 429f4c6d120d6f4784d7104a05782bfb035ec97a Mon Sep 17 00:00:00 2001 From: thelissimus Date: Tue, 11 Nov 2025 14:44:21 +0500 Subject: [PATCH 4/4] add: lean resources --- proof-assistants.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/proof-assistants.md b/proof-assistants.md index 76f325b..2e3de42 100644 --- a/proof-assistants.md +++ b/proof-assistants.md @@ -6,10 +6,24 @@ Isbot assistenti (Inglizchada "proof assistant"), yohud (interaktiv) teorema isb - [Veb sahifa](https://wiki.portal.chalmers.se/agda/pmwiki.php) +TODO: talk about Cubical Agda + ## Lean - [Veb sahifa](https://lean-lang.org/) +### Resurslar + +#### Kitoblar + +- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) +- [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/) +- [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) + +#### Interaktiv kurslar + +- [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/NNG4) + ## Rocq - [Verb sahifa](https://rocq-prover.org/)