philzook58/compact-php

A proof of a finitary pigeon hole principle via compactness and the infinitary version, in Lean.

This repository is not active