Skip to content
@LLM4Rocq

LLM4Rocq

README.md

Code

  • Pytanque is a Python API for lightweight communication with the Rocq proof assistant via coq-lsp.
  • NLIR leverages LLMs' natural language reasoning ability for theorem proving with the Rocq interactive theorem prover .
  • miniF2F-rocq provides a translation in Rocq of the miniF2F benchmarks in Lean and Isabelle.
  • Rocq-MCP is a Model Context Protocol (MCP) server that provides tools for interacting with the Rocq/Coq proof assistant (based on Pytanque).
  • Babel-Formal translates proofs between Rocq and Lean by leveraging proof terms.
  • LLM4Docq is a collaborative project to add docstrings to MathComp.
  • CRRRocq stands for C(hain of thoughts) R(etrieval Assisted Generation) R(ecursive) Rocq. It combines chain of thoughts with RAG and tool calling to generate proofs in interaction with the Rocq prover.

Publications

Pinned Loading

  1. nlir nlir Public

    Automatic theorem proving via natural language reasoning with LLMs

    Python 22 1

  2. miniF2F-rocq miniF2F-rocq Public

    A Rocq version of the miniF2F dataset

    Rocq Prover 23

  3. pytanque pytanque Public

    Python API for lightweight communication with the Rocq proof assistant

    Python 14 5

Repositories

Showing 10 of 17 repositories
  • 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.

    LLM4Rocq/rocq-ml-toolbox’s past year of commit activity
    Python 1 MIT 0 0 0 Updated Feb 25, 2026
  • pytanque Public

    Python API for lightweight communication with the Rocq proof assistant

    LLM4Rocq/pytanque’s past year of commit activity
    Python 14 Apache-2.0 5 0 1 Updated Feb 18, 2026
  • LLM4Docq-MathComp Public

    Automatic docstring generation of mathcomp using LLMs.

    LLM4Rocq/LLM4Docq-MathComp’s past year of commit activity
    Python 1 MIT 0 0 0 Updated Feb 5, 2026
  • 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

    LLM4Rocq/babel-formal’s past year of commit activity
    Python 2 MIT 0 0 0 Updated Jan 29, 2026
  • coq-lsp Public Forked from rocq-community/rocq-lsp

    Visual Studio Code Extension and Language Server Protocol for Coq

    LLM4Rocq/coq-lsp’s past year of commit activity
    OCaml 0 LGPL-2.1 51 0 0 Updated Nov 27, 2025
  • crrrocq-mini Public Forked from LLM4Rocq/crrrocq

    The goal of this repository is to explore an agentic approach for theorem proving in Rocq.

    LLM4Rocq/crrrocq-mini’s past year of commit activity
    Jupyter Notebook 1 1 0 0 Updated Nov 24, 2025
  • .github Public

    Publications

    LLM4Rocq/.github’s past year of commit activity
    0 0 0 0 Updated Nov 6, 2025
  • LLM4Docq-header Public

    The goal of this repository is to work collaboratively on MathComp documentation for LLM4Docq.

    LLM4Rocq/LLM4Docq-header’s past year of commit activity
    0 1 0 0 Updated Oct 30, 2025
  • miniF2F-rocq Public

    A Rocq version of the miniF2F dataset

    LLM4Rocq/miniF2F-rocq’s past year of commit activity
    Rocq Prover 23 MIT 0 2 0 Updated Oct 27, 2025
  • deep-premise-research Public

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

    LLM4Rocq/deep-premise-research’s past year of commit activity
    Python 0 MIT 0 0 0 Updated Oct 24, 2025
View all repositories

Top languages

Loading…

Most used topics

Loading…