A Rocq version of the miniF2F dataset

Exploring RL methods for writing proofs in Rocq.

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

Slides and handwritten notes on the course on models of programming languages

The math library of Lean 4

High level commands to declare a hierarchy based on packed classes

A generic goal preprocessing tool for proof automation tactics in Coq

Stable sort algorithms and their stability proofs in Rocq

Mathematical Components

A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]

Mathematical Components compliant Analysis Library

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]

Ring, field, lra, nra, and psatz tactics for Mathematical Components

Parsing library based on Earley Algorithm

Asymptotic reasoning with bigenough

Micromega tactics for Mathematical Components

Rocq RFCs: documents to discuss changes to the Rocq Prover

https://math-comp.github.io/

Coq/MathComp course for 2020 VU

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

The (very) small kernel of the LaTTe proof assistant

Docker images of coq-mathcomp [maintainer=?]

proof script associated to tutorial material

A proof of Abel-Ruffini theorem.

A Rocq formalization of information theory and linear error-correcting codes

Mathematics of Robotic Manipulation using Rocq and MathComp