Sleeping
Babel Proof Translator
💻
Translate proof between Lean 4 and Rocq prover
Théo Stoskopf PRO
theostos
AI & ML interests
None yet
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
datasets
8
theostos/crrracq
Viewer
•
Updated
•
3.5M
•
7
theostos/llm4docq-mathcomp
Viewer
•
Updated
•
22.8k
•
10
theostos/llm4docq-coq
Viewer
•
Updated
•
2.3k
•
5
theostos/mizarify-eval
Viewer
•
Updated
•
100
•
5
theostos/mini-zBoolQ
Viewer
•
Updated
•
388
•
2
theostos/mini-zMMLU
Viewer
•
Updated
•
387
•
2
theostos/mini-zSlimOrca
Viewer
•
Updated
•
677
•
2
theostos/mini-zSQuAD
Viewer
•
Updated
•
783
•
2