Skip to content

@LLM4Rocq LLM4Rocq

Change the repository type filter

All

    Repositories list

    26 repositories

    • mathcomp-eulerian

      Public
      Rocq Prover
      •
      Apache License 2.0
      •0•0•0•0•Updated May 4, 2026May 4, 2026

    • rocq-mcp

      Public
      MCP server for the Rocq prover
      Python
      •
      Apache License 2.0
      •8•27•0•2•Updated May 4, 2026May 4, 2026

    • mathcomp-qbs

      Public
      Rocq Prover
      •
      Other
      •0•0•0•0•Updated Apr 30, 2026Apr 30, 2026

    • pytanque

      Public
      Python API for lightweight communication with the Rocq proof assistant
      Python
      •
      Apache License 2.0
      •6•18•1•1•Updated Apr 18, 2026Apr 18, 2026

    • 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•1•0•0•Updated Apr 16, 2026Apr 16, 2026

    • LLM4Docq

      Public
      Automatic docstring generation based on the rocq-ml-toolbox.
      Python
      •
      Apache License 2.0
      •0•0•0•0•Updated Apr 16, 2026Apr 16, 2026

    • Pile-of-rocq

      Public
      Pile of Rocq dataset generation, based on Rocq-ml-toolbox
      Python
      •
      MIT License
      •0•0•0•0•Updated Apr 16, 2026Apr 16, 2026

    • mathcomp-kummer

      Public
      Formalization of Kummer's theorem
      Rocq Prover
      •
      Apache License 2.0
      •0•1•0•0•Updated Apr 15, 2026Apr 15, 2026

    • .github

      Public
      Publications
      0•0•0•0•Updated Apr 8, 2026Apr 8, 2026

    • miniF2F-rocq

      Public
      A Rocq version of the miniF2F dataset
      coqdatasetrocq
      coqdatasetrocq
      Rocq Prover
      •
      MIT License
      •0•23•1•1•Updated Apr 8, 2026Apr 8, 2026

    • rocq-skills

      Public
      Python
      •
      Apache License 2.0
      •0•5•0•0•Updated Apr 2, 2026Apr 2, 2026

    • rocq-agent

      Public
      Apache License 2.0
      •0•0•0•0•Updated Apr 1, 2026Apr 1, 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
      Python
      •
      MIT License
      •0•2•0•0•Updated Mar 30, 2026Mar 30, 2026

    • CombiBench-rocq

      Public
      Rocq version of the Lean CombiBench
      Apache License 2.0
      •0•0•0•0•Updated Mar 27, 2026Mar 27, 2026

    • Putnam2025-Rocq

      Public
      Putnam 2025 formalized in Rocq
      Rocq Prover
      •
      Apache License 2.0
      •0•5•0•0•Updated Mar 24, 2026Mar 24, 2026

    • LLM4Docq-MathComp

      Public
      Automatic docstring generation of mathcomp using LLMs.
      Python
      •
      MIT License
      •0•1•0•0•Updated Feb 5, 2026Feb 5, 2026

    • coq-lsp

      Public
      Visual Studio Code Extension and Language Server Protocol for Coq
      OCaml
      •
      GNU Lesser General Public License v2.1
      •53•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•1•0•0•Updated Nov 24, 2025Nov 24, 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

    • 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

    • crrrocq

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

    • nlir

      Public
      Automatic theorem proving via natural language reasoning with LLMs
      Python
      •
      Apache License 2.0
      •1•22•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 en…
      OCaml
      •
      GNU Lesser General Public License v2.1
      •725•0•0•0•Updated Mar 28, 2024Mar 28, 2024

    • ReProver

      Public
      Retrieval-Augmented Theorem Provers for Lean
      Python
      •
      MIT License
      •70•1•0•0•Updated Jan 17, 2024Jan 17, 2024
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.