AI Tools & Models

A hand-curated guide to proof assistants, AI coding agents, LLMs, and research tools — kept up to date.

Sections

Math & theorem proving

Lean & MathlibProof assistant and programming language, with the large Mathlib formal-math library.formal math A

Aristotle (Harmonic)AI mathematician that writes Lean 4 formally-verified proofs (IMO-gold level).AI prover R

Rocq (Coq)Interactive theorem prover for writing and checking formal proofs.verification I

IsabelleGeneric proof assistant with strong proof automation (Sledgehammer).automation

Research & writing

Prism (OpenAI)AI workspace for scientific writing and research, integrated with LaTeX.AI writing P

PerplexityAI answer engine for research with cited, real-time web search.AI search O

Overleaf (LaTeX)Collaborative online LaTeX editor for papers and notes.LaTeX

Coding agents & AI assistants

Claude CodeAgentic coding in the terminal and IDE.agentic CLI O

OpenAI CodexOpenAI's agentic coding tool, in the terminal, IDE and cloud.agentic coding G

GitHub CopilotAI assistant in your editor: completions, chat and an agent mode.IDE assistant G

Google AntigravityGoogle's agentic development platform and AI-first IDE.agentic IDE C

CursorAI-first code editor with in-context edits and agents.AI editor A

AiderAI pair programming from the command line, git-aware.open-source CLI M

ManusAutonomous general-purpose agent with its own browser, terminal and files.autonomous agent

Large language models

ChatGPT (OpenAI)GPT-series models for chat, reasoning and coding.frontier C

Claude (Anthropic)Models strong at reasoning, long-context work and coding.reasoning & code G

Gemini (Google)Google's multimodal models, integrated across Workspace and Android.multimodal G

Grok (xAI)xAI's models with real-time access to X.real-time L

Llama (Meta)Meta's open-weight model family.open weights M

Mistral (Le Chat)Open-weight and frontier models from Mistral AI.open weights D

DeepSeekOpen, reasoning-focused models from DeepSeek.open reasoning Q

Qwen (Alibaba)Alibaba's open-weight, multilingual model family.open, multilingual X

Xiaomi MiMoXiaomi's open-source (MIT) models, strong at coding and agentic tasks.open weights

AI for science & literature

ElicitAI research assistant that finds and summarizes academic papers.lit review C

ConsensusEvidence-based answers drawn directly from research papers.evidence search S

Semantic ScholarAI-powered search across 200M+ academic papers.paper search C

Connected PapersVisual citation-graph explorer to map a research area.citation graph F

FutureHouseAI agents for literature search and scientific discovery.AI scientist

Model hubs & local AI

Hugging FaceHub for open models, datasets and demos.model hub O

OllamaRun open LLMs locally with a single command.local LLMs L

LM StudioDesktop app to download and run models locally.local LLMs O

OpenRouterOne API and marketplace across many model providers.model API V

vLLMHigh-throughput inference and serving engine for LLMs.serving

Benchmarks & leaderboards

LMArena (Chatbot Arena)Human-vote head-to-head Elo rankings of chat models.human votes A

Artificial AnalysisIndependent comparisons of model quality, speed and price.comparisons E

Epoch AIData and trends tracking AI progress over time.trends & data S

SWE-benchBenchmark for coding agents on real GitHub issues.coding bench A

Aider leaderboardPolyglot benchmark ranking models on code editing.coding bench