Pinned Loading

1. LLM4Rocq/rocq-ml-toolbox LLM4Rocq/rocq-ml-toolbox Public

   A toolbox providing Rocq environment generation, an inference server, and project-parsing tools for ML-oriented interaction with the Rocq prover.

   Python

2. LLM4Rocq/deep-premise-research LLM4Rocq/deep-premise-research Public

   The goal of this repository is to explore an agentic approach for premise selections in Lean 4 and Rocq codebase.

   Python

3. LLM4Rocq/babel-formal LLM4Rocq/babel-formal Public

   The goal of this repository is to explore the translation from Rocq/Coq and Lean 4 terms to sequence of tactics in the same language

   Python 1

4. LLM4Rocq/LLM4Docq LLM4Rocq/LLM4Docq Public

   Automatic docstring generation of mathcomp using LLMs.

   Python 1

5. small-pytanque-tp small-pytanque-tp Public

   TP for hands-on session at AI and Maths conference (@PSL)

   Jupyter Notebook 4 1

6. LLM4Rocq/crrrocq LLM4Rocq/crrrocq Public

   Python 5 1