Automating proofs of lattice inequalities in Coq

Theorem-proving using Reinforcement Learning and Duality

December 2019

Proof by duality is heavily employed in pen-and-paper proofs in lattice and order theory. Since the duality lemma is often heavily utilized in lattice theory, we developed a Coq tactic that can apply the duality lemma.

We also developed a reinforcement learning agent in Coq that, without the aid of neural networks or human training data, can prove basic lattice equalities and inequalities. Once the agent was equipped with our duality tactic, the agent could prove theorems in a single step if its dual statement has already been proven in the Coq context. We hope this work is a first step to bringing that proof tactic to formalized, automated, and artificially intelligent proofs.

Read the full paper here.

Code Repository: The code for this project is available on It consists of the Coq files that allow you to prove a statement in lattice theory if the dual of the statement already exists in the Coq context.
Acknowledgements: The Coq code on lattice theory builds on the lattice theory code of other researchers. I did this project as part of my research at UNAM under the guidance of Prof. Favio Ezequiel Miranda Perea and Prof. Lourdes del Carmen González Huesca.