alaingiorgetti edited this page Sep 14, 2018 · 5 revisions

Formal Combinatorics


By "formal combinatorics" we mean studying combinatorics with a computer. This research activity includes the widespread use of a computer algebra system, but also programming of algorithms for the bounded-exhaustive or random generation of combinatorial objects, and implementation of exact or asymptotic formulas for their number for various size parameters, in various formal languages. Less popular are the uses of a proof assistant or an automatic prover to demonstrate combinatorial theorems or properties of combinatorial programs with a computer.

This project gathers contributions in formal combinatorics.


enum is a library of formally verified enumeration programs, still under development. The current release contains enumeration programs in Why3. Clone or download the project Then read the file Why3/



  • Rémi Lazarini, master student, University of Franche-Comté, 2018
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.