20+ Claude Code agentlari birgalikda ishlash: Open Source Theorem Proving

Sun'iy intellekt agentlari yordamida teoremalarni isbotlash

Claude Code agentlari Lean 4 va Ensue Memory Network yordamida teoremalarni isbotlashda hamkorlik qilmoqda. Bu texnologiya multi-agent collaborative theorem proving deb nomlanadi.

Qanday boshlash kerak

• elan (Lean version manager) ni o'rnating: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
• Lean projectini yaratib, Mathlib ni o'rnating: lake new my-project math
• Rust ni o'rnating: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
• Ensue API kalitini oling va git clone git@github.com:mutable-state-inc/lean-collab.git

Claude Code agentlarini ishga tushirish

Claude Code agentlarini ishga tushirish uchun quyidagi buyruqlarni bajarish kerak:

• ./bin/lc init --create-root --theorem "∀ x ∈ [0,π], sin(x) ≥ (2/π)x" --hypotheses "x : ℝ;;hx : x ∈ Set.Icc 0 Real.pi"
• ./bin/lc status
• ./bin/lc listen --prefix proofs/

Maslahatlar

• Max 20x hisobidan foydalaning
• Boshqa Claude Code oynasini ochib, progressni kuzatib boring
• Kamroq ishchilar bilan boshlang
• Loop-lardan ehtiyot bo'ling