Sleeping
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 dataset
5 days ago
theostos/crrracq
published
a dataset
5 days ago
theostos/crrracq
updated
a dataset
21 days ago
theostos/llm4docq-mathcomp
Organizations
spaces
6
Sleeping
Babel SSReflect
📚
Translate vanilla Rocq into SSReflect proof
Sleeping
LLM4Docq Retrieval
👁
Search for MathComp element using natural language query
Runtime error
LLM4Docq Annotator
🐠
Annotate Rocq code automatically, description ↔ statement
Sleeping
LLM4Docq Cosim
🐨
FAISS-index
Sleeping
Rocq Server
🐠
Rocq server
models
7
theostos/babel-ssreflect-fp8
33B
•
Updated
•
6
theostos/babel-translate-fp8
33B
•
Updated
•
4
theostos/LLM4Docq-annotator-fp8
33B
•
Updated
•
4
theostos/LLM4Docq-annotator
33B
•
Updated
•
3
theostos/babel-translate
33B
•
Updated
•
9
theostos/babel-ssreflect
33B
•
Updated
•
7
theostos/zLlamask
Updated
•
4
datasets
8
theostos/crrracq
Viewer
•
Updated
•
3.5M
•
6
theostos/llm4docq-mathcomp
Viewer
•
Updated
•
22.8k
•
92
theostos/llm4docq-coq
Viewer
•
Updated
•
2.3k
•
18
theostos/mizarify-eval
Viewer
•
Updated
•
100
•
31
theostos/mini-zBoolQ
Viewer
•
Updated
•
388
•
8
theostos/mini-zMMLU
Viewer
•
Updated
•
387
•
9
theostos/mini-zSlimOrca
Viewer
•
Updated
•
677
•
10
theostos/mini-zSQuAD
Viewer
•
Updated
•
783
•
13