diff --git a/proof-assistants.md b/proof-assistants.md
new file mode 100644
index 0000000..2e3de42
--- /dev/null
+++ b/proof-assistants.md
@@ -0,0 +1,33 @@
+# Isbot assistentlari
+
+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
+
+- [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/)
+
+## Isabelle
+
+- [Verb sahifa](https://isabelle.in.tum.de/)