thery Goto Github PK

jspeanoware

Javascript version of peaoware

lc0

The rewritten engine, originally for tensorflow. Now all other backends have been ported here.

lemonde

les problèmes proposés par le journal Le Monde en Coq

libdq

Library for creating and manipulating dual quaternions.

math-comp

Mathematical Components

mathcomp-extra

Extra contribution for mathcomp

metric

a classical formalization of metric spaces

mf

A Coq library for multivalued functions.

minirubik

Solving the mini Rubik (2x2) in Coq

multinomials

Multinomials for Ssreflect

nlcertify

NLCertify is a software package for handling formal certification of nonlinear inequalities

note

odd-order

The formal proof of the Odd Order Theorem

opam-coq-archive

Archive for all Coq related OPAM packages organized in various repositories

peanoware

plouffe

Computing Pi decimal using Plouffe Formula in Coq

poltac

Tactic for polynomial manipulations

proviola-source

Proviola, a tool for proof reanimation.

puzzle_cube

A formalisation in Coq of a simple puzzle

repo-stable

The repository for stable Coq packages.

repo-unstable

The repository for development packages.

rlzrs

basic realizability for Coq

robbins

Proof in Coq that all Robbins algebras are Boolean algebras

selinger

Formalisation of Selinger proof about quantum gate

sudoku

Sudoku in Coq

sudoku-1

A certified Sudoku solver in Coq [maintainer=@siraben]

t2048

a version of the 2048 game for Coq

tarjan

Formalization of Tarjan 72 algorithm in Coq with mathematical components and ssreflect

thery.github.io

tictactoetutor