Repositories list

• coq-tactician-api

  Public
  An API for interfacing with Coq through Tactician by external agents

  machine-learningcoqtheorem-proving+ 3coq-pluginproof-synthesisproving-agent

  Python

  •

  MIT License

  •1•2•2•0•Updated Feb 5, 2025Feb 5, 2025

• coq-tactician

  Public
  A Seamless, Interactive Tactic Learner and Prover for Coq

  machine-learningcoqtheorem-proving+ 2coq-pluginproof-synthesis

  OCaml

  •

  MIT License

  •20•58•36•1•Updated Jan 31, 2025Jan 31, 2025

• benchmark-data

  Public
  Coq

  •1•0•0•0•Updated Dec 29, 2024Dec 29, 2024

• coq-graph2tac-trained

  Public
  Shell

  •1•1•0•0•Updated Dec 28, 2024Dec 28, 2024

• graph2tac

  Public
  Graph-based neural tactic prediction models for Coq.

  Jupyter Notebook

  •

  Apache License 2.0

  •6•0•0•0•Updated Dec 19, 2024Dec 19, 2024

• coq-tactician.github.io

  Public
  Tactician's website

  HTML

  •1•0•0•4•Updated Dec 13, 2024Dec 13, 2024

• benchmark-system

  Public
  OCaml

  •1•4•1•0•Updated Sep 12, 2024Sep 12, 2024

• platform

  Public
  Multi platform setup for Coq, Coq libraries and tools

  Shell

  •

  Creative Commons Zero v1.0 Universal

  •50•1•0•0•Updated Jul 25, 2024Jul 25, 2024

• coq-tactician-dummy

  Public
  A minimal dummy version of Tactician to depend on for public packages

  Coq

  •

  MIT License

  •0•0•0•0•Updated Apr 11, 2024Apr 11, 2024

• coq-tactician-stdlib

  Public
  This package will recompile Coq's standard library with support for Tactician.

  Makefile

  •

  GNU Lesser General Public License v2.1

  •2•1•0•0•Updated Oct 17, 2023Oct 17, 2023

• .github

  Public
  0•0•0•0•Updated Oct 8, 2022Oct 8, 2022