🚀 راهنمای استفاده از سرویس‌های محاسباتی و هوش مصنوعی

🔗 ۱. روش‌های دسترسی

🔑 ۲. دریافت رمز عبور

• 📧 ارسال ایمیل به m.amintoosi@um.ac.ir
• 💬 ارسال پیام در پیام‌رسان بله به آی‌دی @mamintoosi

⚙️ ۳. تنظیمات مرورگر برای نمایش LEAN InfoView

برای مشاهده پنجره LEAN InfoView (که اطلاعات اثبات‌ها و اهداف را نشان می‌دهد)، باید تنظیمات امنیتی مرورگر را تغییر دهید:

📚 ۴. آشنایی با Lean

• Lean یک زبان برنامه‌نویسی کاربردی و اثبات‌کننده قضایا است که برای ریاضیات رسمی‌شده طراحی شده است.
• Mathlib بزرگترین کتابخانه ریاضیات رسمی‌شده برای Lean است که شامل قضایا، تعاریف و اثبات‌های گسترده در شاخه‌های مختلف ریاضیات می‌باشد.
• این محیط برای کار بر روی پروژه‌های پژوهشی مرتبط با ریاضیات رسمی، اثبات‌های خودکار و توسعه کتابخانه‌های ریاضی بسیار مفید است.

🎯 ۵. کاربردها در دانشکده علوم ریاضی

• ✅ پژوهش در زمینه ریاضیات رسمی‌شده (Formalized Mathematics)
• ✅ توسعه کتابخانه‌های ریاضی برای پروژه‌های تحقیقاتی
• ✅ آموزش اثبات‌های دقیق ریاضی با استفاده از کامپیوتر
• ✅ همکاری در پروژه‌های متن‌باز مرتبط با Lean و Mathlib
• ✅ آشنایی با سیستم‌های اثبات‌کننده قضایا (Theorem Provers)

🔗 ۱. روش‌های دسترسی از طریق مرورگر

👤 ۲. نحوه ورود

🔌 ۳. دسترسی برنامه‌نویسی (Ollama API)

برای اتصال از طریق کد پایتون یا R (مناسب برای ساخت Agent، خودکارسازی، و افزونه‌هایی مانند Continue و Cline در VSCode):

📍 آدرس سرور Ollama

🐍 نمونه کد پایتون

from ollama import Client

# --- از داخل JupyterHub ---
client = Client(host='http://host.docker.internal:11434')

# --- از کامپیوتر شخصی (داخل دانشکده) ---
# client = Client(host='http://172.21.129.16:11434')

# --- از کامپیوتر شخصی (خارج از دانشکده با Tailscale) ---
# client = Client(host='http://math-gpu-server.tailde35cf.ts.net:11434')

model = 'qwen3:8b'
prompt = "Explain the difference between supervised and unsupervised learning in one paragraph."

response = client.chat(model=model, messages=[
    {'role': 'user', 'content': prompt}
])

print(response['message']['content'])

📊 نمونه کد R

library(ollamar)

# --- از داخل JupyterHub ---
OLLAMA_HOST <- "http://host.docker.internal:11434"

# --- از کامپیوتر شخصی (داخل دانشکده) ---
# OLLAMA_HOST <- "http://172.21.129.16:11434"

# --- از کامپیوتر شخصی (خارج از دانشکده با Tailscale) ---
# OLLAMA_HOST <- "http://math-gpu-server.tailde35cf.ts.net:11434"

model <- "qwen3:8b"
prompt <- "Explain the difference between supervised and unsupervised learning in one paragraph."

response <- chat(
  model = model,
  messages = list(list(role = "user", content = prompt)),
  output = "text",
  host = OLLAMA_HOST
)

cat(response)

📚 ۴. مدل‌های زبانی موجود

حدود ۱۰۰ گیگابایت مدل زبانی روی سرور قرار داده شده است. این مدل‌ها نسبت به مدل‌های بزرگ آنلاین (مانند ChatGPT و Claude) توانایی کمتری دارند، اما برای کارهای زیر در محیط محلی (بدون اینترنت بین‌الملل و بدون پرداخت هزینه API) مفید هستند:

• 🔬 اجرای پروژه‌های پژوهشی (مانند مقاله Nature: Large language models for scientific discovery)
• 🤖 ساخت Agentهای هوشمند برای خودکارسازی وظایف
• 🔐 چت با مدل محلی
• 💻 کدنویسی و دیباگ با افزونه‌هایی مانند Continue و Cline در VSCode

📋 لیست مدل‌های دانلود شده

🔗 روش‌های دسترسی

🎯 کاربردها

• 🔍 کشف مخزن‌های اخیر GitHub در زمینه یادگیری ماشین، بینایی ماشین و بهینه‌سازی ترکیبی
• 📄 جستجوی مقالات arxiv-sanity برای یافتن مقالات مرتبط
• 🤖 تولید ایده‌های پژوهشی با استفاده از مدل‌های زبانی محلی (LM Studio یا Ollama)
• 📊 مدیریت و مشاهده تاریخچه ایده‌ها تولید شده
• 📅 زمان‌بندی اجرای خودکار روزانه

⚙️ تنظیمات

برای تغییر تنظیمات (مانند پرسش جستجو، مدل زبانی، و زمان‌بندی)، از طریق رابط وب اقدام کنید یا فایل config.json را ویرایش نمایید.

🔗 روش‌های دسترسی