theo.stoskopf theostos

Pinned Loading

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

   Python 1

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

   Python

3. 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 2

4. Automatic docstring generation of mathcomp using LLMs.

   Python 1

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

   Jupyter Notebook 4 1