Skip to content

@LLM4Rocq LLM4Rocq

Change the repository type filter

All

    Repositories list

    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.
      Python
      •
      MIT License
      •0•0•0•0•Updated Dec 20, 2025Dec 20, 2025

    • pytanque

      Public
      Python API for lightweight communication with the Rocq proof assistant
      Python
      •
      Apache License 2.0
      •3•10•1•0•Updated Dec 19, 2025Dec 19, 2025

    • coq-lsp

      Public
      Visual Studio Code Extension and Language Server Protocol for Coq
      OCaml
      •
      GNU Lesser General Public License v2.1
      •51•0•0•0•Updated Nov 27, 2025Nov 27, 2025

    • crrrocq-mini

      Public
      The goal of this repository is to explore an agentic approach for theorem proving in Rocq.
      Jupyter Notebook
      •1•0•0•0•Updated Nov 24, 2025Nov 24, 2025

    • 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
      •
      MIT License
      •0•1•0•0•Updated Nov 18, 2025Nov 18, 2025

    • .github

      Public
      Publications
      0•0•0•0•Updated Nov 6, 2025Nov 6, 2025

    • LLM4Docq-header

      Public
      The goal of this repository is to work collaboratively on MathComp documentation for LLM4Docq.
      1•0•0•0•Updated Oct 30, 2025Oct 30, 2025

    • miniF2F-rocq

      Public
      A Rocq version of the miniF2F dataset
      coqdatasetrocq
      Rocq Prover
      •
      MIT License
      •0•22•0•0•Updated Oct 27, 2025Oct 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.
      Python
      •
      MIT License
      •0•0•0•0•Updated Oct 24, 2025Oct 24, 2025

    • LLM4Docq

      Public
      Automatic docstring generation of mathcomp using LLMs.
      Python
      •
      MIT License
      •0•1•0•0•Updated Oct 13, 2025Oct 13, 2025

    • crrrocq

      Public
      Python
      •1•5•1•0•Updated Oct 7, 2025Oct 7, 2025

    • rocq-mcp

      Public
      MCP server for the Rocq prover
      Python
      •
      Apache License 2.0
      •0•11•0•0•Updated Sep 15, 2025Sep 15, 2025

    • nlir

      Public
      Automatic theorem proving via natural language reasoning with LLMs
      Python
      •
      Apache License 2.0
      •1•19•1•1•Updated May 16, 2025May 16, 2025

    • S1-mini

      Public
      Python
      •0•0•0•0•Updated Apr 18, 2025Apr 18, 2025

    • RL-rocq

      Public
      Exploring RL methods for writing proofs in Rocq.
      Python
      •
      MIT License
      •0•1•0•0•Updated Apr 14, 2025Apr 14, 2025

    • coq

      Public
      Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
      OCaml
      •
      GNU Lesser General Public License v2.1
      •704•0•0•0•Updated Mar 28, 2024Mar 28, 2024

    • ReProver

      Public
      Retrieval-Augmented Theorem Provers for Lean
      Python
      •
      MIT License
      •68•1•0•0•Updated Jan 17, 2024Jan 17, 2024