Running on Zero
Agents
Babel Proof Translator
💻
Translate proof between Lean 4 and Rocq prover
Théo Stoskopf PRO
theostos
P(doom) 10%
AI & ML interests
None yet
Recent Activity
updated a model about 1 hour ago
theostos/qwen-3.5-babel-9b-sft-agent published a model about 1 hour ago
theostos/qwen-3.5-babel-9b-sft-agent updated a model 16 days ago
theostos/qwen-3.5-babel-4b-sft-agentOrganizations
spaces 6
Running on Zero
Agents
Babel SSReflect
📚
Translate vanilla Rocq into SSReflect proof
Runtime error
Agents
LLM4Docq Retrieval
👁
Search for MathComp element using natural language query
Runtime error
Agents
LLM4Docq Annotator
🐠
Annotate Rocq code automatically, description ↔ statement
Sleeping
LLM4Docq Cosim
🐨
FAISS-index
Sleeping
Rocq Server
🐠
Rocq server
models 17
theostos/qwen-3.5-babel-9b-sft-agent
Text Generation • 9B • Updated
theostos/qwen-3.5-babel-4b-sft-agent
Text Generation • 4B • Updated • 323
theostos/qwen-3.5-babel-2b-sft-agent
Text Generation • 2B • Updated • 328
theostos/qwen-3.5-babel-0.8b-sft-agent
Text Generation • 0.8B • Updated • 323
theostos/qwen-3.5-babel-27b-sft
Text Generation • 27B • Updated • 377
theostos/qwen-3.5-babel-9b-sft
Text Generation • 9B • Updated • 371
theostos/qwen-3.5-babel-4b-sft
Text Generation • 4B • Updated • 344
theostos/qwen-3.5-babel-2b-sft
Text Generation • 2B • Updated • 320
theostos/qwen-3.5-babel-0.8b-sft
Text Generation • 0.8B • Updated • 286
theostos/babel-ssreflect-fp8
33B • Updated • 11
datasets 11
theostos/integral-tp-retrieval-cache
Updated • 4
theostos/pile-of-rocq
Viewer • Updated • 47.3M • 1.64k
theostos/crrracq
Viewer • Updated • 3.5M • 14
theostos/llm4docq-mathcomp
Viewer • Updated • 22.8k • 7
theostos/llm4docq-coq
Viewer • Updated • 2.3k • 2
theostos/mizarify-eval
Viewer • Updated • 100 • 18
theostos/mizarify-train
Viewer • Updated • 1k • 11
theostos/mini-zBoolQ
Viewer • Updated • 388 • 8
theostos/mini-zMMLU
Viewer • Updated • 387 • 4
theostos/mini-zSlimOrca
Viewer • Updated • 677 • 10