Running on Zero
Agents
Babel Proof Translator
💻
Translate proof between Lean 4 and Rocq prover
Théo Stoskopf PRO
theostos
AI & ML interests
None yet
Recent Activity
updated a model about 8 hours ago
theostos/qwen-3.5-babel-27b-sft published a model about 9 hours ago
theostos/qwen-3.5-babel-27b-sft updated a model about 9 hours ago
theostos/qwen-3.5-babel-9b-sftOrganizations
spaces 6
Sleeping
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
Running
LLM4Docq Cosim
🐨
FAISS-index
Sleeping
Rocq Server
🐠
Rocq server
models 13
theostos/qwen-3.5-babel-27b-sft
Text Generation • 27B • Updated
theostos/qwen-3.5-babel-9b-sft
Text Generation • 9B • Updated
theostos/qwen-3.5-babel-4b-sft
Text Generation • 4B • Updated
theostos/qwen-3.5-babel-2b-sft
Text Generation • 2B • Updated
theostos/qwen-3.5-babel-0.8b-sft
Text Generation • 0.8B • Updated
theostos/babel-ssreflect-fp8
33B • Updated • 5
theostos/babel-translate-fp8
33B • Updated • 4
theostos/LLM4Docq-annotator-fp8
33B • Updated • 5
theostos/LLM4Docq-annotator
33B • Updated • 4
theostos/babel-translate
33B • Updated • 3
datasets 11
theostos/integral-tp-retrieval-cache
Updated • 66
theostos/pile-of-rocq
Viewer • Updated • 47.3M • 2.59k
theostos/crrracq
Viewer • Updated • 3.5M • 12
theostos/llm4docq-mathcomp
Viewer • Updated • 22.8k • 4
theostos/llm4docq-coq
Viewer • Updated • 2.3k • 10
theostos/mizarify-eval
Viewer • Updated • 100 • 13
theostos/mizarify-train
Viewer • Updated • 1k • 6
theostos/mini-zBoolQ
Viewer • Updated • 388 • 4
theostos/mini-zMMLU
Viewer • Updated • 387 • 5
theostos/mini-zSlimOrca
Viewer • Updated • 677 • 8