Skip to content

@LLM4Rocq LLM4Rocq

Change the repository type filter

All

    Repositories list

    33 repositories

    • icones-rocq

      Public
      Rocq Prover
      •
      Other
      •0•0•0•0•Updated Aug 7, 2026Aug 7, 2026

    • mathcomp-skills

      Public
      A Claude Code skill for writing idiomatic MathComp / MathComp-Analysis Rocq code.
      Shell
      •
      Apache License 2.0
      •0•3•0•0•Updated Aug 5, 2026Aug 5, 2026

    • .github

      Public
      Publications
      0•0•0•0•Updated Aug 5, 2026Aug 5, 2026

    • rocq-mcp

      Public
      MCP server for the Rocq prover
      Python
      •
      Apache License 2.0
      •13•40•2•3•Updated Aug 5, 2026Aug 5, 2026

    • Putnam2025-Rocq

      Public
      Putnam 2025 formalized in Rocq
      Rocq Prover
      •
      Apache License 2.0
      •0•6•0•0•Updated Aug 3, 2026Aug 3, 2026

    • rocqet-search

      Public
      Semantic search over Rocq/Coq mathematical libraries.
      Python
      •
      Apache License 2.0
      •0•0•0•0•Updated Jul 25, 2026Jul 25, 2026

    • miniF2F-rocq

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

    • graph-theory-rocq

      Public
      Rocq Prover
      •
      Apache License 2.0
      •0•2•4•0•Updated Jul 18, 2026Jul 18, 2026

    • rocq-mcp-evolve

      Public
      Minimal MCP for rocq
      OCaml
      •
      Apache License 2.0
      •0•3•0•0•Updated Jul 9, 2026Jul 9, 2026

    • small-prime-gap

      Public
      Rocq Prover
      •0•0•0•0•Updated Jul 8, 2026Jul 8, 2026

    • rocq-workbook

      Public
      Rocq translation of a subset of the Lean workbook
      Python
      •0•0•0•0•Updated Jun 27, 2026Jun 27, 2026

    • mathcomp-eulerian

      Public
      Rocq Prover
      •
      Apache License 2.0
      •0•3•0•0•Updated Jun 23, 2026Jun 23, 2026

    • digraph-theory

      Public
      Rocq Prover
      •
      Apache License 2.0
      •0•1•0•0•Updated Jun 12, 2026Jun 12, 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•4•0•0•Updated May 19, 2026May 19, 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•2•0•0•Updated May 19, 2026May 19, 2026

    • mathcomp-qbs

      Public
      Rocq Prover
      •
      Other
      •0•0•0•0•Updated May 15, 2026May 15, 2026

    • pytanque

      Public
      Python API for lightweight communication with the Rocq proof assistant
      Python
      •
      Apache License 2.0
      •6•20•0•1•Updated Apr 18, 2026Apr 18, 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

    • rocq-skills

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

    • CombiBench-rocq

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

    • LLM4Docq-MathComp

      Public
      Automatic docstring generation of mathcomp using LLMs.
      Python
      •
      MIT License
      •0•2•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
      •63•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•6•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•23•1•1•Updated May 16, 2025May 16, 2025

    • S1-mini

      Public
      Python
      •0•0•0•0•Updated Apr 18, 2025Apr 18, 2025
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.